about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-05-22 06:07:50 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-05-22 06:07:50 +0000
commit21bbf33d53209f1bc30562b1bebb9f568c5c7360 (patch)
tree0aba734899f6364e62878dc518cf98911817b610
parent7855e18aa4c702a92c6aa6ec75c9dd2a07ea1ca4 (diff)
downloadklee-21bbf33d53209f1bc30562b1bebb9f568c5c7360.tar.gz
Some minor web page tweaks.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72247 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r--www/GetStarted.html14
-rw-r--r--www/index.html13
-rw-r--r--www/install.html72
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>