Validity checking of void pointers in contracts
#6375
Conversation
SaswatPadhi
requested review from
peterschrammel and
tautschnig
as code owners
SaswatPadhi
force-pushed
the
void-ptr-validate
branch
from
7f7744a to
7c8b893
Compare
| if(opt_size_of_deref.has_value()) | ||
| validity_checks.push_back(good_pointer_def(pointer, ns)); | ||
| else | ||
| validity_checks.push_back(false_exprt()); |
There was a problem hiding this comment.
Could you add a comment here this could happen in case of void pointers?
Codecov Report
@@ Coverage Diff @@
## develop #6375 +/- ##
========================================
Coverage 75.91% 75.91%
========================================
Files 1517 1517
Lines 164024 164026 +2
========================================
+ Hits 124515 124517 +2
Misses 39509 39509
Continue to review full report at Codecov.
|
|
Closing this PR after offline discussions. We would want to raise an error in this case and not ignore it as invalid. |
|
It would be neat if we could retain the change you made do src/util/pointer_predicates.cpp in whatever comes next. |
PR #6365 introduced
good_pointer_defchecks on all pointers being deref'ed within code contracts. However, this function crashes onvoidpointers.In this PR, we consider deref'ing
voidpointers as "invalid" as opposed to crashing.The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/My commit message includes data points confirming performance improvements (if claimed).White-space or formatting changes outside the feature-related changed lines are in commits of their own.