-
Notifications
You must be signed in to change notification settings - Fork 274
Make pointer-primitive-check a no-op when behaviour is always defined #6491
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
Make pointer-primitive-check a no-op when behaviour is always defined #6491
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #6491 +/- ##
========================================
Coverage 76.09% 76.09%
========================================
Files 1548 1548
Lines 166328 166327 -1
========================================
+ Hits 126563 126568 +5
+ Misses 39765 39759 -6
Continue to review full report at Codecov.
|
1f2a160
to
4a6be48
Compare
4a6be48
to
dc12412
Compare
pointer_object, pointer_offset have well-defined behaviour even when the input is an unconstrained pointer: the result is equally unconstrained. Regression tests are updated to reflect the reduced number of checks generated by --pointer-primitive-check. Note that the patterns in pointer-primitive-check-03 never were effective as they were placed in the patterns-not-to-seen section of test.desc while also missing proper parenthesis escaping (making the patterns trivially non-matching). Fixes: diffblue#6238
dc12412
to
be35b6c
Compare
- `__CPROVER_same_object` | ||
|
||
Using them on invalid pointers, however, may still be unintended in user | ||
programs. |
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.
This is really helpful; thanks for adding it.
Is the patch coverage number correct? If so it would be good to be over the current average. |
Looking at GitHub's annotated diff, nothing in the diff is called out as being uncovered. Also, it would be very much surprising if any C/C++ changes were not covered. Perhaps Codecov measures the coverage against all lines in the diff, including changes to documentation? I wasn't able to figure out from Codecov's documentation how this is computed. |
pointer_object, pointer_offset have
well-defined behaviour even when the input is an unconstrained pointer:
the result is equally unconstrained.
Regression tests are updated to reflect the reduced number of checks
generated by --pointer-primitive-check. Note that
the patterns in pointer-primitive-check-03 never were effective as they
were placed in the patterns-not-to-seen section of test.desc while also
missing proper parenthesis escaping (making the patterns trivially
non-matching).