Function pointer restrictions: support labels in JSON input #6610
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
tautschnig
force-pushed
the
bugfixes/6609-restrictions-json
branch
from
9413956 to
27a04a5
Compare
tautschnig
requested review from
chrisr-diffblue and
martin-cs
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6610 +/- ##
===========================================
+ Coverage 76.62% 76.64% +0.01%
===========================================
Files 1578 1578
Lines 181180 181210 +30
===========================================
+ Hits 138833 138884 +51
+ Misses 42347 42326 -21
Continue to review full report at Codecov.
|
chrisr-diffblue
approved these changes
Jan 25, 2022
|
|
||
| restrict_function_pointers( | ||
| ui_message_handler, goto_model, function_pointer_restrictions); | ||
| restrict_function_pointers(ui_message_handler, goto_model, options); |
No changes in behaviour: this commit just moves the pointer-name parsing introduced in 771a153 to a function of its own. This is to prepare for a fix of diffblue#6609: the same name parsing also needs to be added to function-pointer-restriction parsing from JSON files. To enable this code move, the exception class is moved to the global scope.
This is a follow-up fix to 771a153, which added support for labels as function-pointer identifiers. That commit, however, failed to consider JSON input, and instead only resulted in support for command-line specified restrictions. Fixes: diffblue#6609
Rather than requiring users to (necessarily!) make at least two calls, just process what users actually have available (a goto model and some command line options).
tautschnig
force-pushed
the
bugfixes/6609-restrictions-json
branch
from
27a04a5 to
73980e4
Compare
chrisr-diffblue
approved these changes
Jan 26, 2022
| /// Parse \p candidate to distinguish whether it refers to a function pointer | ||
| /// symbol directly (as produced by \ref label_function_pointer_call_sites), or | ||
| /// a source location via its statement label. In the latter case, resolve the | ||
| /// name to the underlying function pointer symbol. |
There was a problem hiding this comment.
Brilliant, thanks :-)
|
I can confirm this solves the problem we had using restrictions files with Kani (formerly RMC). |
Merged
4 tasks
peterschrammel
approved these changes
Feb 1, 2022
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.
This is a follow-up fix to 771a153, which added support for
labels as function-pointer identifiers. That commit, however, failed to
consider JSON input, and instead only resulted in support for
command-line specified restrictions.
Fixes: #6609
Please review commit-by-commit.