Hi > My initial thought was to get the information from .cov files generated for > each test cases but, differently from what I was expecting, it is not the > case that the three test cases explore the same lines: > TC #1: 7,8,12,13,22,30,31,32,35 > TC #2: 7,8,11,30,31,32,35 > TC #3: 7,8,11,30,31,32,35
The lines are not the same because you've used short circuit operators in the if statement so there are more branches than you might think. I would advise that you take a look at the LLVM IR for your program because will shows you the branches that KLEE actually sees. If you look inside ``klee-last`` there is a file called assembly.ll . This is the program that KLEE interpreted as LLVM IR. You can read the LLVM IR file but some times it can be quite hard to visualise what's going on so you can use LLVM's opt tool to visualise this IR file $ opt -analyze -view-cfg klee-last/assembly.ll which will launch an application (e.g. xdotpy if it in your PATH when you built LLVM) to view the cfg. It will launch a program one at a time for each function in assembly.ll or $ opt -analyze -dot-cfg klee-last/assembly.ll which will spit out a .dot file per function. You can then open the file of interest using a graphviz viewer of your choice (I prefer xdotpy). This will show you the control flow graph for each function definition in assembly.ll If you are unfamiliar with LLVM IR take a look at the Language Reference ( http://llvm.org/docs/LangRef.html ) Hope that helps. Thanks, Dan. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
