[llvm-commits] [klee] r72305 - in /klee/trunk/www: GetStarted.html tutorial-1.html

[Cristian Cadar]

Author: cristic
Date: Fri May 22 19:44:00 2009
New Revision: 72305

URL: http://llvm.org/viewvc/llvm-project?rev=72305&view=rev
Log:
Updates to install guide and first tutorial.

Modified:
    klee/trunk/www/GetStarted.html
    klee/trunk/www/tutorial-1.html

Modified: klee/trunk/www/GetStarted.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/GetStarted.html?rev=72305&r1=72304&r2=72305&view=diff

==============================================================================
--- klee/trunk/www/GetStarted.html (original)
+++ klee/trunk/www/GetStarted.html Fri May 22 19:44:00 2009
@@ -34,8 +34,9 @@
 <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 @@
 
   <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>

Modified: klee/trunk/www/tutorial-1.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/tutorial-1.html?rev=72305&r1=72304&r2=72305&view=diff

==============================================================================
--- klee/trunk/www/tutorial-1.html (original)
+++ klee/trunk/www/tutorial-1.html Fri May 22 19:44:00 2009
@@ -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>