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/tutorial-1.html | 27 +++++++++++++++++++++++----
 1 file changed, 23 insertions(+), 4 deletions(-)

(limited to 'www/tutorial-1.html')

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