Skip to content

Replace __VERIFIER_assume() by an implementation

🤖 SoSy-Bot 🤖 requested to merge remove__VERIFIER_assume into master

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:

Merge request reports