From 5134f5c11d976f32636fcb825356206be834f194 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Sat, 23 May 2009 00:44:00 +0000
Subject: Updates to install guide and first tutorial.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72305 91177308-0d34-0410-b5e6-96231b3b80d8
---
 www/GetStarted.html |  9 +++++----
 www/tutorial-1.html | 27 +++++++++++++++++++++++----
 2 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/www/GetStarted.html b/www/GetStarted.html
index 88fb05dc..890510ab 100644
--- a/www/GetStarted.html
+++ b/www/GetStarted.html
@@ -34,8 +34,9 @@ them soon.<p>
 <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
+  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>
@@ -74,11 +75,11 @@ necessary, but KLEE runs very slowly in Debug mode).
 
   <li>Build KLEE (from the KLEE source directory):
     <div class="instr">
-      make
+      make ENABLE_OPTIMIZED=1
     </div>
   </li>
 
-  <li>Run DejaGNU and unit tests to verify your build:
+  <li>Run the regression suite to verify your build:
     <div class="instr">
       make check<br>
       make unittests<br>
diff --git a/www/tutorial-1.html b/www/tutorial-1.html
index 8307e69c..389359b2 100644
--- a/www/tutorial-1.html
+++ b/www/tutorial-1.html
@@ -27,6 +27,7 @@
       else return 0;
   } </pre>
 
+  You can find the entire code for this example <a href="code-examples/demo.c">here</a>. 
 
   <h2>Marking input as symbolic</h2> 
 
@@ -147,14 +148,32 @@
 
   While we can run the test cases generated by KLEE on our program by
   hand, (or with the help of an existing test infrastructure), KLEE
-  provides a convenient <i>replay driver</i>, which simply replaces
+  provides a convenient <i>replay library</i>, which simply replaces
   the call to <tt>klee_make_symbolic</tt> with a call to a function
-  that assigns to our input the value stored in the .bout file:
+  that assigns to our input the value stored in the .bout file.
+
+  To use it, simply link your program with the <tt>libkleeRuntest</tt>
+  library and set the <tt>KLEE_RUNTEST</tt> environment variable to
+  point to the name of the desired test case:
 
   <pre class="output">
-  $ gcc ... </pre>
+  $ gcc path/to/klee/Release/lib/libkleeRuntest.dylib demo.c
+  $ KLEE_RUNTEST=klee-last/test000001.bout ./a.out 
+  $ echo $?
+  1
+  $ KLEE_RUNTEST=klee-last/test000002.bout ./a.out 
+  $ echo $?
+  0
+  $ KLEE_RUNTEST=klee-last/test000003.bout ./a.out
+  $ echo $?
+  0 </pre>
+
+  As expected, our program returns 1 when running the first test case
+  (which contains the lowercase letter <tt>'b'</tt>), and 0 when
+  running the other two (which don't contain lowercase letters).
+
+  <br/><br/>
 
-  
 </div>
 </body>
 </html>
-- 
cgit 1.4.1