Replace __VERIFIER_assume() by an implementation
Created by: skanav
This PR is created as an alternate solution for the issue #1035 (closed) instead of PR #1040
It does semantically the same thing, but instead of replacing the __VERIFIER_assume
call with an if condition we now replace it with a function call: assume_cycle_if_not
for the memory cleanup tasks and assume_abort_if_not
all the remaining tasks.
As a first step the tasks for valid-memcleanup
were identified and these files were updated manually.
As a second step all the remaining files were updated using the following script:
find . -name "*.[hci]" -print0 | \
xargs -0 perl -0777 -pi -e \
's/void __VERIFIER_assume([^;]*);/void abort(void); \nvoid assume_abort_if_not(int cond) { \n if(!cond) {abort();}\n}/ ; \
s/__VERIFIER_assume/assume_abort_if_not/g'
Fixes: #1035 (closed) Closes #1040
Please have a look at #1035 (closed) for more details.
Added by dbeyer 2020-01-09:
- Fixes #1031 (closed)
- Solves #578 (closed)