diff options
Diffstat (limited to 'www/klee-files.html')
| -rw-r--r-- | www/klee-files.html | 137 |
1 files changed, 0 insertions, 137 deletions
diff --git a/www/klee-files.html b/www/klee-files.html deleted file mode 100644 index 299f593b..00000000 --- a/www/klee-files.html +++ /dev/null @@ -1,137 +0,0 @@ -<!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> |