[klee-dev] Help with collecting coverage information

Daniel Liew daniel.liew at imperial.ac.uk
Thu Aug 21 18:10:12 BST 2014


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.




More information about the klee-dev mailing list