diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2009-05-21 06:59:38 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2009-05-21 06:59:38 +0000 |
| commit | 69c4c5548d5e366113b376d77520df7f79142403 (patch) | |
| tree | 36833ece3be585b1c8e16217c070fa3c54c8f285 /www/klee-files.html | |
| parent | 467108ce9b81a4f57f2fb52d1a35759d4bd053a1 (diff) | |
| download | klee-69c4c5548d5e366113b376d77520df7f79142403.tar.gz | |
Started web pages describing the main KLEE tools, and the main files
generated by KLEE. Small updates to the CSS file and tutorials.html git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72208 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'www/klee-files.html')
| -rw-r--r-- | www/klee-files.html | 78 |
1 files changed, 78 insertions, 0 deletions
diff --git a/www/klee-files.html b/www/klee-files.html new file mode 100644 index 00000000..a15b0c0b --- /dev/null +++ b/www/klee-files.html @@ -0,0 +1,78 @@ +<!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>KLEE Generated Files</h1> + <!--*********************************************************************--> + + <h2>Standard Files</h2> + These 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">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> Kleaver files</h2> + + <ol> + <li><b>test<NNN>.pc</b> files: + </li> + <li><b>queries.pc:</b> + </li> + </ol> + +</div> +</body> +</html> |