about summary refs log tree commit diff homepage
path: root/www/GetStarted.html
blob: 88fb05dc804ceef5c4df24ef38a4d25f30a05782 (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
<!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>. It
  is important to do this first so that it 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
    </div>
  </li>

  <li>Run DejaGNU and unit tests 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>