Open salvadorer opened 11 months ago
From a cursory reading of your program, your __VERIFIER_assume(tmp_ndt_4 == 1);
statement is telling CBMC to explore only the state space where tmp_ndt_4
is equal to 1
. In those states, tmp_ndt_4 > 0
is equivalent to 1 > 0
which is trivially true.
Your __VERIFIER_assume(0)
is basically cutting off paths from that state space exploration, which is causing a different path to be explored (to my understanding, one in which the first if
antecedent is followed, resulting in tmp_ndt_4
being nondeterministic).
For the branch in which the condition in the if is evaluated to false
it makes sense, but to my understanding CBMC should explore all branches and for the other branch (where the if-condition evaluates to true
) the assertion might not hold (for both versions of the first assumption). Therefore I don't understand why the assertion is not reported.
Hi, I tested your program and I can say that the behaviour you experimented is a current bug of CBMC.
Here's a simplified version of your program:
#include <assert.h>
extern void __VERIFIER_assume(int cond);
extern int __VERIFIER_nondet_int(void);
int main(void) {
int if_condition = __VERIFIER_nondet_int();
if (if_condition) {
goto label;
}
int var = __VERIFIER_nondet_int();
__VERIFIER_assume (var == 1);
label:
assert(var > 0);
return 0;
}
Running CBMC should return verification failure and the trace to obtain this is by having condition = 1
, then as we skip the initialization of var
var
has a nondeterministic value, so it is possible to reach assert(var > 0
with var < 0
.
For some reason it seems that the simplification step of CBMC adds a non-guarded (by the if condition
) assignment var = 1
.
For the moment it is possible to get the expected VERIFICATION FAILED
result by adding the --no-simplify
argument to CBMC.
Actually it seems to be a problem also when removing the __VERIFIER_assume
and initializing var
to 1
in the first place as follows:
#include <assert.h>
extern void __VERIFIER_assume(int cond);
extern int __VERIFIER_nondet_int(void);
int main(void) {
int if_condition = __VERIFIER_nondet_int();
if (if_condition) {
goto label;
}
int var = 1;
label:
assert(var > 0);
return 0;
}
Also in this case the variable var
should have a nondeterministic value as its initialization is only in the control-flow where condition
is false, so when condition
is true it should fail violating the assertion.
This happens irregardless of --no-simplify
and --no-propagation
.
We might have to move all declarations (not the initialisations!) to the beginning of a block while producing the GOTO program.
We might have to move all declarations (not the initialisations!) to the beginning of a block while producing the GOTO program.
I agree as:
Still it has to be investigated why in the original program the simplifier adds an unguarded var = 1
after the __VERIFIER_assume(var == 1);
.
Dear all, looking at the following program, I am asking myself why CBMC does not report the assertion failure:
I know that jumping over a variable declaration and reading the variable can give any value, so I thought the assertion should fail. The observed behavior is especially surprising since changing the first assumption to __VERIFIER_assume(0) would give the warning about the assertion as expected.
Calling "cbmc test.c" gives: ** Results: test.c function main [main.assertion.1] line 13 assertion tmp_ndt_4 > 0: SUCCESS
** 0 of 1 failed (1 iterations) VERIFICATION SUCCESSFUL
CBMC version: 5.95.0 Operating system: Ubuntu