[klee-dev] Effect of --optimize

[Eduardo R B Marques]

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 <f.busse at imperial.ac.uk> wrote:
> 
> Hi,
> 
> 
> On Thu, 23 Sep 2021 17:03:03 +0100
> Eduardo R B Marques <ebmarques at fc.up.pt> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev