-
Notifications
You must be signed in to change notification settings - Fork 280
goto-harness: use __CPROVER_(de)?allocate, not malloc/free #8684
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
goto-harness: use __CPROVER_(de)?allocate, not malloc/free #8684
Conversation
We can compile __CPROVER_allocate, but wouldn't be able to handle ALLOCATE(type, size, bool).
402ebc3
to
c6270fe
Compare
c6270fe
to
fe673e6
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8684 +/- ##
===========================================
- Coverage 80.39% 80.39% -0.01%
===========================================
Files 1688 1688
Lines 207392 207383 -9
Branches 73 73
===========================================
- Hits 166739 166731 -8
+ Misses 40653 40652 -1 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Do not use C-specific functions when amending GOTO programs. Fixes: diffblue#8681
fe673e6
to
f06afc4
Compare
--harness-type call-function --function test_fn | ||
^\[test_fn.assertion.1\] line 11 assertion \(a == \(int \*\)0\) \|\| \(\*a != 5\): FAILURE$ | ||
^\*\* 1 of \d+ failed | ||
VERIFICATION FAILED |
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.
Shouldn't this test pass?
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.
Not in this restricted setting of that particular regression test as we don't actually do contracts instrumentation. The full workflow now does pass.
Do not use C-specific functions when amending GOTO programs.
Fixes: #8681