search

izlatkin / HornLauncher

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

[tool tg] low coverage for gauss_sum.i.p+lhb-reducer #20

Closed izlatkin closed 3 years ago

izlatkin commented 3 years ago

https://github.com/sosy-lab/sv-benchmarks/blob/99d37c5b4072891803b9e5c154127c912477f705/c/loop-new/gauss_sum.i.p%2Blhb-reducer.c coverage is expected to be higher and covered conditions main__sum = main__sum + main__i; main__i = main__i + 1; label_87:; if (main__i <= main__n) { main__sum = main__sum + main__i; main__i = main__i + 1;

gauss_sum.i.p+lhb-reducer.smt2.txt log.txt image

grigoryfedyukovich commented 3 years ago

The SMT file has a lot fewer branches than we see in the source code... perhaps because SeaHorn optimized it a lot. Anyway, the coverage should be much better now.

izlatkin commented 3 years ago

yes, coverage it definatly better image