esbmc / esbmc

The efficient SMT-based context-bounded model checker (ESBMC)
http://esbmc.org/
Other
290 stars 94 forks source link

[Coverage] Assertion Instances Coverage: 1100% #2063

Open lucasccordeiro opened 1 week ago

lucasccordeiro commented 1 week ago

$ esbmc main.c --assertion-coverage --unwind 10

#include <assert.h>
int main () {
  int a , x , y = 0 , z;
  a = nondet_int();
  x = nondet_int();
  z = nondet_int();
  if (a > 25000 && x == 30000) {
    while (y++ < z) {
      if (y % 3 != 0) {
        a++;
        x--;
      } else {
      a--; x++;
      }
      assert (a != x);
   }
  }
}
[Coverage]

Total Asserts: 1
Total Assertion Instances: 1
Reached Assertion Instances: 11
Assertion Instances Coverage: 1100%

VERIFICATION FAILED
lucasccordeiro commented 6 days ago

@ChenfengWei0: Did you have a chance to look at this issue?

ChenfengWei0 commented 6 days ago

@ChenfengWei0: Did you have a chance to look at this issue?

Will check after finishing the test-comp stuff