[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