Semantics of assert statements
salvadorer opened this issue · 2 comments
salvadorer commented
Hey,
I'm working with CBMC 5.95.1 and I noticed that CBMC does not add asserted conditions to the path conditions. For e.g.:
#include <assert.h>
extern int __VERIFIER_nondet_int(void);
int main() {
int x = __VERIFIER_nondet_int();
assert(x < 0);
assert(x <= 0);
}
CBMC would report a warning about both assertions but there's actually no value for x that can trigger the second assertion.
tautschnig commented
That's indeed true, see #5866: we might revisit this at some point, but until then please redefine the assert
macro like this:
#undef assert
#define assert(C) __CPROVER_assert((C), "assertion"); __CPROVER_assume(C)