blob: 299f593be3f12e34f30fd3b1575cd6748c7b6e51 (
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
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>
|
