blob: 5c445059e763fe88c7b770323865c2d167cdeb91 (
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
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" />
<title>KLEE - Getting Started</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>Getting Started: Building and Running KLEE</h1>
<!-- <p>FIXME: Intro and disclaimer.</p> -->
<h2 id="build">Building KLEE and Working with the Code</h2>
<p>If you would like to try KLEE, the current procedure for building is
below.</p>
KLEE is built on LLVM; the first steps are to get a working LLVM
installation. See <a href="http://llvm.org/docs/GettingStarted.html">Getting
Started with the LLVM System</a> for more information.
<p><b>NOTE:</b> KLEE is only currently tested on Linux and Darwin x86-32 targets,
using LLVM top-of-tree. KLEE will not work with an older LLVM (e.g., 2.5), and is
currently untested on any x86-64 target, although we hope to add support for
them soon.<p>
<ol>
<li>Install llvm-gcc:</li>
<ul>
<li>Download and install the LLVM 2.5 release of <tt>llvm-gcc</tt>
from <a href="http://llvm.org/releases/download.html">here</a>. Add
<tt>llvm-gcc</tt> to your <tt>PATH</tt>. It
is important to do this first so that <tt>llvm-gcc</tt> is found in
subsequent <tt>configure</tt> steps. <tt>llvm-gcc</tt> will be used
later to compile programs that KLEE can execute.</li>
</ul>
<li><a href="http://www.llvm.org/docs/GettingStarted.html#checkout">Checkout
and build LLVM</a> from SVN head (LLVM 2.5 will not work):
<div class="instr">
svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm <br>
cd llvm <br>
./configure --enable-optimized <br>
make
</div>
(the <tt>--enable-optimized</tt> configure argument is not
necessary, but KLEE runs very slowly in Debug mode).
</li>
<li>Checkout KLEE (to any path you like):
<div class="instr">
svn co http://llvm.org/svn/llvm-project/klee/trunk klee
</div>
</li>
<li>Configure KLEE (from the KLEE source directory):
<div class="instr">
./configure --with-llvm=<i>path/to/llvm</i>
</div>
<p>This assumes that you compiled LLVM in-place. If you used a
different directory for the object files then use:
<div class="instr">
./configure --with-llvmsrc=<i>path/to/llvm/src</i> --with-llvmobj=<i>path/to/llvm/obj</i>
</div>
</li>
<li>Build KLEE (from the KLEE source directory):
<div class="instr">
make ENABLE_OPTIMIZED=1
</div>
</li>
<li>Run the regression suite to verify your build:
<div class="instr">
make check<br>
make unittests<br>
</div>
</li>
<li>You're ready to go! Go to the <a href="Tutorials.html">Tutorials</a> page
to try KLEE.</li>
</ol>
<!-- <h2> Full Installation </h2> -->
<!-- If you need uCLibc and/or POSIX support add <i>-with-uclibc</i> -->
<!-- and <i>-enable-posix-runtime</i> to configure. Thus, to enable -->
<!-- both, replace step 3 above with: -->
<!-- <div class="instr"> -->
<!-- ./configure -with-llvm=<i>path/to/llvm</i> -with-uclibc -enable-posix-runtime ENABLE_OPTIMIZED=1 -->
<!-- </div> -->
<!-- However, note that... -->
</div>
</body>
</html>
|
