Thanks a lot, -klee-call-optimisation=false works. Are there any other side effects of optimisation worth noting?
(btw clang also removes the call to match irrelevant with -O2, I am going to check there is an option to disable that kind of optimisation within clang as well, I suppose there is one ). Best, Eduardo > On 23 Sep 2021, at 17:45, Frank Busse <[email protected]> wrote: > > Hi, > > > On Thu, 23 Sep 2021 17:03:03 +0100 > Eduardo R B Marques <[email protected]> wrote: > >> $ klee --optimize --only-output-states-covering-new Regexp.bc >> … >> KLEE: Using STP solver backend >> >> KLEE: done: total instructions = 5 >> KLEE: done: completed paths = 1 >> KLEE: done: partially completed paths = 0 >> KLEE: done: generated tests = 1 > > This is a bug. The call of match() is completely removed from main() in > the bitcode. Using "--klee-call-optimisation=false" might help. > > > Kind regards, > > Frank > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
