diff options
| -rw-r--r-- | www/GetStarted.html | 14 | ||||
| -rw-r--r-- | www/index.html | 13 | ||||
| -rw-r--r-- | www/install.html | 72 |
3 files changed, 15 insertions, 84 deletions
diff --git a/www/GetStarted.html b/www/GetStarted.html index 5f28b1d3..88fb05dc 100644 --- a/www/GetStarted.html +++ b/www/GetStarted.html @@ -19,13 +19,17 @@ <h2 id="build">Building KLEE and Working with the Code</h2> -<p>If you would like to check out and build KLEE, the current procedure is as -follows:</p> - +<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> @@ -37,7 +41,7 @@ Started with the LLVM System</a> for more information. </ul> <li><a href="http://www.llvm.org/docs/GettingStarted.html#checkout">Checkout - and build LLVM</a> from SVN head: + 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> @@ -64,7 +68,7 @@ necessary, but KLEE runs very slowly in Debug mode). <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> + ./configure --with-llvmsrc=<i>path/to/llvm/src</i> --with-llvmobj=<i>path/to/llvm/obj</i> </div> </li> diff --git a/www/index.html b/www/index.html index 4b9e5f3b..e789bf56 100644 --- a/www/index.html +++ b/www/index.html @@ -16,17 +16,16 @@ <!--*********************************************************************--> <p>KLEE is a symbolic virtual machine built on top of - the <a href="http://llvm.org">LLVM</a> compiler infrastructure.</p> + the <a href="http://llvm.org">LLVM</a> compiler infrastructure, and available + under the UIUC open source license.</p> - <p>Stay tuned for more information on public availability. For now, - there is some information available on - the <a href="http://checking.stanford.edu/wiki/Klee">Stanford - Checking Group wiki</a>.</p> - - <p>For more information, see + <p>For more information on what KLEE is and what it can do, see the <a href="http://llvm.org/pubs/2008-12-OSDI-KLEE.html">OSDI 2008</a> paper.</p> + <p>If you are interested in trying it yourself, please + see <a href="GetStarted.html">Getting Started</a>.</p> + <!-- <p>FIXME: Somewhere need to describe what KLEE can do well and what is more "experimental" or research level. This should also address how KLEE could be used by outside groups (i.e. kleaver).</p> --> diff --git a/www/install.html b/www/install.html deleted file mode 100644 index 79aeb4b1..00000000 --- a/www/install.html +++ /dev/null @@ -1,72 +0,0 @@ -<!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 Installation Guide</h1> - <!--*********************************************************************--> - - <h2> Minimal Installation </h2> - <ol> - <li> Obtain the current version - of <a href="http://llvm.org/releases/download.html#svn">LLVM via - SVN</a>. Build the release version of LLVM and install the GCC - front end as well. Follow the instructions - at <a href="http://llvm.org/docs/GettingStarted.html">Getting - Started with the LLVM System</a>.</li> - - <li> Obtain the current version of KLEE via SVN (readonly access): - <div class="code">svn co http://llvm.org/svn/llvm-project/klee/trunk klee</div> - </li> - - <li> Configure KLEE: - <div class="code"> - ./configure --with-llvm=<i>path/to/llvm ENABLE_OPTIMIZED=1</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="code"> - ./configure --with-llvmsrc=<i>path/to/llvm/src</i>--with-llvmobj=<i>path/to/llvm/obj</i> - </div> - </li> - - <li> Build the release version of KLEE: - <div class="code"> - make - </div> - </li> - - <li> Run the test suite. You should have no unexpected failures.but - please <a href="bugs.html">report</a> any such failures. - <div class="code"> - make test - </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="code"> --> -<!-- ./configure -with-llvm=<i>path/to/llvm</i> -with-uclibc -enable-posix-runtime ENABLE_OPTIMIZED=1 --> -<!-- </div> --> -<!-- However, note that... --> - -</div> -</body> -</html> |