[klee-dev] Use of --optimize flag

Sean Bartell sean at yotann.org
Thu Jun 23 21:42:29 BST 2016


RAJDEEP MUKHERJEE on 2016-06-23:
>In default mode, klee uses dfs search strategy with incremental solving.
>What additional optimisations does Klee perform with the --optimize switch ?

The --optimize switch causes KLEE to run standard compiler optimizations on the 
subject program before starting to execute it. It's similar to compiling the 
subject program with an option like -O2. One difference is that if you tell 
KLEE to link the subject with uclibc or the POSIX runtime, KLEE will do 
optimization *after* linking, which gives extra opportunities for inlining.
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list