blob: a15b0c0b96ae62789ffe0ab88fac8ac7a1e5f358 (
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
|
<!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>
|
