clean up goto_symex function calls #6406
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
kroening
commented
Oct 21, 2021
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
The method is no longer in use.
kroening
force-pushed
the
symex_function_call
branch
2 times, most recently
from
9666dab to
5f4a4cf
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6406 +/- ##
===========================================
+ Coverage 75.97% 75.98% +0.01%
===========================================
Files 1523 1523
Lines 164201 164284 +83
===========================================
+ Hits 124758 124839 +81
- Misses 39443 39445 +2
Continue to review full report at Codecov.
|
kroening
requested review from
peterschrammel,
romainbrenguier and
tautschnig
as code owners
tautschnig
approved these changes
Oct 21, 2021
Collaborator
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
I would appreciate if the commit "change signature of goto_symext::symex_function_call" could be merged with the change to symex_function_call_symbol: the latter has a proper commit message and merging them will avoid some unnecessary back&forth.
…on_call_symbol This changes the signatures of symex_function_call and symex_function_call_symbol, which can now enforce the fact that the function to be executed is given as symbol expression using typing.
This both renames the method symex_function_call_code and changes its signature, to better reflect the ordering of steps when executing function calls.
kroening
force-pushed
the
symex_function_call
branch
from
5f4a4cf to
3d64049
Compare
Collaborator
Author
Done. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.