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.
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
