diff options
| -rw-r--r-- | www/GetStarted.html | 9 | ||||
| -rw-r--r-- | 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> |