-
Notifications
You must be signed in to change notification settings - Fork 72
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Type-safe global query system #1423
base: master
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice! I think we should add this to the documentation.
Also, why is it necessary to stop recording per loop termination information here? I think such information can be very helpful, e.g., when debugging or potentially in the future, when we may want to slice out a program containing only the part for which we could not show termination.
Could we maybe think of better names for these things? I think Also, |
Just |
True, maybe give it |
Queries like
WarnGlobal
andInvariantGlobal
are only used globally in dummyctx
. Moreover, they haveObj.t
arguments which are unsafe.Every analysis lifter which adds its own global unknowns must have special cases for converting such arguments for
WarnGlobal
andInvariantGlobal
. If that is forgotten, then Goblint simply segfaults.This PR introduces global queries using a separate
global_query
"transfer" function andgctx
global "context" for the queries, which doesn't require all the dummy data.TODO
InvariantGlobal
query.