diff options
Diffstat (limited to 'www/klee-files.html')
| -rw-r--r-- | www/klee-files.html | 137 |
1 files changed, 137 insertions, 0 deletions
diff --git a/www/klee-files.html b/www/klee-files.html new file mode 100644 index 00000000..299f593b --- /dev/null +++ b/www/klee-files.html @@ -0,0 +1,137 @@ +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" + "http://www.w3.org/TR/html4/strict.dtd"> +<!-- Material used from: HTML 4.01 specs: http://www.w3.org/TR/html401/ --> +<html> +<head> + <META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"> + <title>The KLEE Symbolic Virtual Machine</title> + <link type="text/css" rel="stylesheet" href="menu.css"> + <link type="text/css" rel="stylesheet" href="content.css"> +</head> +<body> +<!--#include virtual="menu.html.incl"--> +<div id="content"> + <!--*********************************************************************--> + <h1>Files generated by KLEE</h1> + <!--*********************************************************************--> + + <h2>Standard Global Files</h2> + + These are global files are always generated on a KLEE execution: + <ol> + <li><b>info</b>: This is a text file containing various information + related to a KLEE run. In particular, it records the exact + command-line with which KLEE was run, and the total time taken by + the execution. E.g.: + <pre class="output"> + $ cat info + klee --write-pcs demo.o + PID: 12460 + Started: 2009-05-20 22:31:41 + BEGIN searcher description + DFSSearcher + END searcher description + Finished: 2009-05-20 22:31:41 + Elapsed: 00:00:00 + KLEE: done: explored paths = 3 + KLEE: done: avg. constructs per query = 6 + KLEE: done: total queries = 3 + KLEE: done: valid queries = 0 + KLEE: done: invalid queriers = 3 + KLEE: done: query cex = 3 + KLEE: done: total instructions = 67 + KLEE: done: completed paths = 3 + KLEE: done: generated tests = 3 </pre> + </li> + + <li><b>warnings.txt</b>: This is a text file containing all warnings emitted by KLEE. + </li> + + <li><b>messages.txt</b>: This is a text file containing all other messages emitted by KLEE. + </li> + + <li><b>assembly.ll</b>: This file contains a human readable version + of the LLVM bitcode executed by KLEE + + <li><b>run.stats</b>: This is a text file containing various + statistics emitted by KLEE. While this file can be inspected + manually, you should use the <a href="klee-tools.html">klee-stats</a> + tool for that.</li> + + <li><b>run.istats</b>: This is a binary file containing global + statistics emitted by KLEE for each line of code in the program. + </li> + + </ol> + + + <h2>Other Global Files</h2> + + <ol> + <li><b>all-queries.pc:</b> This file contains all the queries KLEE + made during execution in the <a href="KQuery.html">KQuery</a> + format. Note these are the queries before any optimisation + (e.g. caching, constraint independence) so it is possible that + some of the queries logged are never executed by KLEE's underlying + solver or are modified before being executed by KLEE's underlying + solver. The generation of this file can be enabled by specifying + the option <tt>--use-query-log=all:pc</tt> to KLEE.</li> + <li><b>all-queries.smt2:</b> This file contains all the queries KLEE made during execution in the <a href="http://www.smtlib.org">SMT-LIBv2</a> + .It contains the same information as <tt>all-queries.pc</tt>. + The generation of this file can be enabled by specifying the option <tt>--use-query-log=all:smt2</tt> to KLEE.</li> + <li><b>solver-queries.pc:</b> This file contains all the queries passed to KLEE's underlying solver during execution in the + <a href="KQuery.html">KQuery</a> format. Note these are the + queries after all optimisations (e.g. caching, constraint + independence) are performed. The generation of this file can be + enabled by specifying the + option <tt>--use-query-log=solver:pc</tt> to KLEE.</li> + <li><b>solver-queries.smt2:</b> This file contains all the queries passed to KLEE's underlying solver during execution in the + <a href="http://www.smtlib.org">SMT-LIBv2</a> + format. It contains the same information as <tt>solver-queries.pc</tt>. + The generation of this file can be enabled by specifying the option <tt>--use-query-log=solver:smt2</tt> to KLEE.</li> + </ol> + + + <h2> Per-path files</h2> + + <ol> + <li> + <b>test<N>.ktest</b>: Contains the test case generated by + KLEE on that path. Use <a href="klee-tools.html">ktest-tool</a> + to read the contents. The generation of <tt>.ktest</tt> files + can be disabled using the <tt>--no-output</tt> option. + </li> + + <li> + <b>test<N>.<error-type>.err</b>: Generated for paths + where KLEE found an error. Contains information about the error + in textual form. + </li> + + <li><b>test<N>.pc:</b> Contains the constraints associated with the given + path, in <a href="KQuery.html">KQuery</a> format. The generation + of these files can be enabled via the <tt>--write-cvcs</tt> flag. + </li> + + <li> + <b>test<N>.cvc:</b> Contains the constraints associated + with the given path, + in <a href="https://sites.google.com/site/stpfastprover/stp-documentation#TOC-The-CVC-language">CVC</a> + format. The generation of these files can be enabled via + the <tt>--write-pcs</tt> flag. (This is the same information as + in the corresponding <tt>.pc</tt> file.) + </li> + <li> + <b>test<N>.smt2:</b> Contains the constraints associated + with the given path, + in <a href="http://www.smtlib.org/">SMT-LIBv2</a> + format. The generation of these files can be enabled via + the <tt>--write-smt2s</tt> flag. (This is the same information as + in the corresponding <tt>.pc</tt> file.) + </li> + </ol> + + +</div> +</body> +</html> |