izlatkin / HornLauncher

scripts and reports for executions seahorn and test generation
0 stars 0 forks source link

[tg tool] low coverage for terminator_02-2 #19

Closed izlatkin closed 2 years ago

izlatkin commented 3 years ago

For https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/loops/terminator_02-2.c coverage is expected to be higher and covered condition line 26 while(x<100 && z>100) image

terminator_02-2.smt2.txt log.txt

grigoryfedyukovich commented 3 years ago

should be fixed

izlatkin commented 3 years ago

It is partially fixed, looks like lines 35-40 should be covered image

all 4 tests contains only static const int inp_14364[] = {};

it is expected both static const int inp_14364[] = {1}; and static const int inp_14364[] = {0};

izlatkin commented 3 years ago

very similar case with https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/trex02-2.c image

izlatkin commented 3 years ago

Need to find SeaHorn option to increase # of rules

grigoryfedyukovich commented 3 years ago

I believe I fixed the issue (for terminator_02).

izlatkin commented 3 years ago

Strange results: image terminator_02-2.smt2_1.txt image terminator_02-2.smt2_2.txt

izlatkin commented 3 years ago

return x => return rand() image terminator_02-2_return.smt2.txt

Coverage diff image image

izlatkin commented 2 years ago

fix, SeaHorn bug related to Error: key \d+ not found