blob: 73ca3535633caa69932ae9191abeb639e7ba3e28 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
<!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>queries.pc:</b> </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>
</ol>
</div>
</body>
</html>
|
