Hi Sang, Originally KLEE explores all possible paths and create an execution tree. But yeah there are some options which optimize the execution tree. During our experiment for a project related to MC/DC, we have noticed such optimization and we had not used that default optimization option. Please check if it works for your case or not. 1. Navigate to: lib/Module/KModule.cpp 2. Comment the line: "pm3.add(createCFGSimplificationPass());" [Line number 368 in my code]
These steps will avoid simplifying the CFG. It is very useful when you have complex Boolean expressions with AND (&&) and OR (||) logical operators. Also, there may be some more simplifications and optimizations by default in KLEE which must have some useful objectives but you may choose to use them or to ignore. Thanks, Sanghu On Fri, Oct 26, 2018 at 7:05 AM Sang Phan <[email protected]> wrote: > Hello, > > The assembly.ll that KLEE generates is much more optimized than the one > generated by opt. > > So what optimization that KLEE uses before the execution, and where in the > source that I can them? > > Thank you, > Sang > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > -- Thanks & Regards, Dr. Sangharatna Godboley, Ph.D. Postdoctoral Research Fellow, NUS Singapore.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
