-
Notifications
You must be signed in to change notification settings - Fork 265
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
Add new function to inline a list of calls in a goto_program #7550
Add new function to inline a list of calls in a goto_program #7550
Conversation
42c2411
to
769098d
Compare
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.
Seems reasonable enough. It feels like the whole goto_inline
infrastructure could do with a tidy up and refactor but that's out of scope for this PR. I get what you are saying about testing but would it be useful to have a unit test for this?
Second the desire for some kind of unit testing. |
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.
Approving module required Doxygen fixes (see CI job).
3275a34
to
717ddea
Compare
@peterschrammel @TGWDB I added a unit test for the new function. |
717ddea
to
d7e2e5d
Compare
This PR a new function in
goto_inline.h
and a new method ingoto_inline_class.h
thatallows to inline a specified set of calls inside a target goto program.
The use case for this is the inlining of function calls in short snippets of goto programs generated during function and loop contract instrumentation, that contain dynamic frame initialisation statements or havoc statements.
The existing inlining functions only allow to inline all calls found in the whole body of a goto function, and do not allow to inline calls inside a small program snippet like needed for contract instrumentation.
The new functions will be exercised/tested as part of the new loop contracts PR #7541.