KLEE

Note: KLEE is not open-source at this this point.

* Installation - READ THIS FIRST

* Tutorial 1

* UsefulOptions

* Other

* Resources (obsolete)

uclibc

We use a modified version of uclibc 0.9.29.

Source access (for members of our group):

svn co svn+ssh://yourname@keeda.stanford.edu/netapp/projects/repositories/uclibc

zcov

zcov is an lcov replacement which supports reporting branch coverage and is intended to be easier to use and work with.

Source access (for members of our group):

svn co svn+ssh://name@keeda.stanford.edu/netapp/projects/repositories/zcov/trunk zcov

Example usage:

$ zcov-scan cu-dev.zcov ~/public/coreutils-6.10.cov
$ zcov-genhtml cu-dev.zcov cu-dev-html

zcov-merge can also be used to combine multiple .zcov files.

zcov can also check that the lines mentioned in the .cov files generated by klee are in fact covered in the gcov output. This is enabled with options to zcov-genhtml, as in:

$ zcov-genhtml --annotate-klee-cov /path/to/testing/directory --strip-cov-path coreutils-6.10.cov cu-dev.zcov cu-dev-html

The first option, --annotate-klee-cov, is a path to a directory which will be recursively searched for .cov files. The second option, --strip-cov-path, is optional. If specified, it should be a the name of a key directory which is used in the file paths. If present in the path, all path components prior to this will be stripped before zcov tries to match the path in the .cov file to a source file on the current filesystem. This can be used to allow coverage information to be generated on platforms or by users who have the sources stored in different locations.

When viewing html files, hit the B key to toggle display/hiding of branches taken/not taken.

Klee (last edited 2009-04-27 02:33:56 by CristianCadar)