[klee-dev] Cloud9 and KLEE - POSIX features

2016-06-23 Thread Marko Dimjašević
Dear KLEE developers, Can anyone comment on what's the connection between the POSIX runtime in KLEE and in Cloud9? As mentioned in a paper on Cloud9: http://doi.acm.org/10.1145/1966445.1966463 Cloud9 builds on KLEE. Have some or all POSIX features from Cloud9 been back-ported to KLEE? The

Re: [klee-dev] Use of --optimize flag

2016-06-23 Thread Sean Bartell
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

Re: [klee-dev] Use of --optimize flag

2016-06-23 Thread Daniel Guo
There is an Optimize.cpp in which various optimizing llvm passes are created, e.g., CFGSimplification, ConstantPropagation, InstructionCombining ... You can find all the passes there, and check how they are created and applied. On Thu, Jun 23, 2016 at 10:14 AM, RAJDEEP MUKHERJEE <

[klee-dev] Use of --optimize flag

2016-06-23 Thread RAJDEEP MUKHERJEE
Hi, I recently ran some experiments with klee with the --optimize switch and without --optimize switch. It seems that the solving using --optimize switch is much faster than without it. In default mode, klee uses dfs search strategy with incremental solving. What additional optimisations does