This repository has been archived by the owner on Oct 3, 2021. It is now read-only.
Replace __VERIFIER_assume() by an implementation #1072
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
dbeyer
changed the title
skanav
force-pushed
the
remove__VERIFIER_assume
branch
from
214f47e
to
a59698b
Compare
|
This does not affect the rules of SV-COMP, so I removed that label. But it makes one rule superfluous ;-) |
dbeyer
approved these changes
Jan 10, 2020
There was a problem hiding this comment.
Reasons for this change:
- The definition of
__VERIFIER_assume(p)in the SV-COMP rules (cycling without termination ifpis not satisfied) is different from what many people expect by intuition (assumption or contract), and from what is implemented in many participating verifiers. - Avoiding this speciality greatly simplifies the rules and the verification tasks.
- The special semantics of
__VERIFIER_assume(p)is not essential to express interesting and practically relevant verification tasks. - Having an assume is practically relevant for verification engineers, thus, we still use a function name that reminds the reader of an
assume, but the functions have definitions and no other special meaning.
lembergerth
added a commit
to lembergerth/sv-benchmarks
that referenced
this pull request
Jul 11, 2020
…_not Implementation of assume_abort_if_not as proposed by sosy-lab#1072 Commands used: 1. Python code used to remove definition of ldv_assume: ``` def remove_assume(content): in_assume = -1 for line in content: if (line.strip() == "void ldv_assume(int expression )"): in_assume = 0 if in_assume < 0 or in_assume > 13: yield line else: in_assume = in_assume + 1 for f in glob.glob(*.c): with open(f) as inp: content = inp.readlines() new_content = list(remove_assume(content)) with open(f, w) as outp: outp.writelines(new_content) ``` 2. Python code used to remove definition of ldv_stop: ``` def remove_stop(content): in_assume = -1 for line in content: if (line.strip() == "void ldv_stop(void)"): in_assume = 0 if in_assume < 0 or in_assume > 8: yield line else: in_assume = in_assume + 1 for f in glob.glob(*.c): with open(f) as inp: content = inp.readlines() new_content = list(remove_stop(content)) with open(f, w) as outp: outp.writelines(new_content) ``` Bash command used to replace occurrences of ldv_assume and ldv_stop and introduce definition of assume_abort_if_not: ``` sed -i *.c \ -e 's/ldv_assume/assume_abort_if_not/g' \ -e '/void ldv_stop(void) ;/d' \ -e 's/ldv_stop()/assume_abort_if_not(0)/g' \ -e 's/void assume_abort_if_not(int expression.*).*;/extern void abort(void);\nvoid assume_abort_if_not(int cond) {\n if(!cond) {abort();}\n}/' ```
This was referenced Dec 9, 2020
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is created as an alternate solution for the issue #1035 instead of PR #1040
It does semantically the same thing, but instead of replacing the
__VERIFIER_assumecall with an if condition we now replace it with a function call:assume_cycle_if_notfor the memory cleanup tasks andassume_abort_if_notall the remaining tasks.As a first step the tasks for
valid-memcleanupwere identified and these files were updated manually.As a second step all the remaining files were updated using the following script:
Fixes: #1035
Closes #1040
Please have a look at #1035 for more details.
Added by dbeyer 2020-01-09: