izlatkin / HornLauncher

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

[tg tool] some of testgen.h do not contains all necessary methods #12

Closed izlatkin closed 3 years ago

izlatkin commented 3 years ago

For example for https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-invariants/eq1.c ['/Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg', '--keys', '15269,15339,3673,2481', 'eq1.smt2']

tg tool returns 7 headers but 3 out of 7 testgen.h contain all four nondet_XXXX methods. Some of them contain only 3 nondet_XXXX methods. For example for testgen_0.h there is no method nondet_2481 such code doesn't not compile "main.c:18:9: error: implicit declaration of function 'nondet_2481'"

Looks like this method was never called during runtime for this test, but it is needed for coverage If added empty method to testgen.h than coverage is following image

izlatkin commented 3 years ago

absent methods could be added as const int nondet_XXXX(){ return rand(); }

grigoryfedyukovich commented 3 years ago

Thanks, will do!

izlatkin commented 3 years ago

eq1.smt2.txt

izlatkin commented 3 years ago

Similar behavior for https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/terminator_02-2.c

/Users/ilyazlatkin/PycharmProjects/aeval/build/tools/tg/tg --keys 4630,4657,14364 terminator_02-2.smt2

terminator_02-2.smt2.txt tg generates 9 tests, none of them contains all 3 nondet_XXXX methods. Some of the headers are empty and contain only #include <stdlib.h>

grigoryfedyukovich commented 3 years ago

Should be fixed in the new commit

izlatkin commented 3 years ago

looks good image