search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
787 stars 255 forks source link

Semantics of assert statements #8223

Closed salvadorer closed 1 week ago

salvadorer commented 4 months ago

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 4 months ago

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)
martin-cs commented 2 months ago

@salvadorer Just for interest, this is why they don't alter the path condition:

https://github.com/diffblue/cbmc/pull/2031 https://github.com/diffblue/cbmc/commit/92b92d6032d4f0492603d2f85db5b52d6798b04c

I'm still reasonably convinced this is the correct design decision.

tautschnig commented 1 week ago

Closing as this is documented behaviour.