> But the output from KLEE indicated that it completed only one path whereas > the program clearly has two paths. Can anyone please explain why this > happened ?
Remember that KLEE executes LLVM IR, not C! You should look at the LLVM IR. If you look (see ``klee-last/assembly.ll``) you'll see that the branch has been lowered to a select instruction (i.e. an if then else instruction). This happens due to the running the pass created by ``createCFGSimplificationPass()`` in ``KModule::prepare(...)`` _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
