Overflow in programs with unreachable property violations
mikhailramalho opened this issue · 9 comments
Both ESBMC and CBMC find overflows in:
s3_clnt_1.BV.c.cil-1a.c
s3_clnt_1.BV.c.cil-2a.c
s3_srvr_1a_alt.BV.c.cil.c
The property file states that there no reachable property violation in the program, but since overflows are UB, the property violation can be reachable somehow.
How should we proceed? Should I create a PR that changes the overflow verdict and removes the reachable safety property?
Can you post some witnesses for the violations?
The usual approach is to make two variants of the tasks, one where the overflow is fixed and true_nooverflow is added to the verdicts, and one where the overflow is unfixed and false_nooverflow is the only verdict.
@mikhailramalho the first two files out of the 3 files mentioned by you are the same. Did you miss something by any chance?
The usual approach is to make two variants of the tasks, one where the overflow is fixed and true_nooverflow is added to the verdicts, and one where the overflow is unfixed and false_nooverflow is the only verdict.
These tasks were created to have the correct verdict as part of the issue #810 . There are already enough tasks related to this file for false_overflow.
regarding the file s3_clnt_1.BV.c.cil-1a.c CPAChecker also produces a different verdict than expected. The following 2 problems were found:
- Overflow at line 307 for the variable
s__s3__tmp__new_cipher__algorithms. The can be resolved by changing its type from int to unsigned. - After making this change we ran the CPAChecker again and it found another problem. Variable
s__s3__flagsis declared at line 30 but is used without initialization. - CPAChecker times out if we change the type of
s__s3__flagsto unsigned and initialize it with__VERIFIER_nondet_uint(). Although I am not sure if we should do this.
@dbeyer I would suggest to remove this task from scoring computation of the competition.
The file s3_srvr_1a_alt.BV.c.cil.c also has the similar problem. After changing the types of six variables from int to unsigned (and also initializing some of them with __VERIFIER_nondet_uint()) solves the problem and the CPAChecker produces the expected verdict.
@dbeyer This task should also be removed from the scoring computation. Or alternatively, it can be modified.
Hi all,
The benchmarks are:
s3_clnt_1.BV.c.cil-1a.c
s3_clnt_1.BV.c.cil-2a.c
s3_srvr_1a_alt.BV.c.cil.c
The witnesses produced from 181579a: witnesses.zip
Please modify s3_srvr_1a_alt.BV.c.cil.c if possible and not sufficiently many variants are available already.
It did not add the fixed/keep tasks. For example there must have been a reason for having both s3_srvr_1a_alt.BV.c.cil.c and s3_srvr_1a.BV.c.cil.c, both with verdicts noverflow=true and unreachcall=true. Now we essentially lost one of them. For the other two tasks it is probably similar