From 5134f5c11d976f32636fcb825356206be834f194 Mon Sep 17 00:00:00 2001 From: Cristian Cadar 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.

  • Install llvm-gcc:
  • @@ -74,11 +75,11 @@ necessary, but KLEE runs very slowly in Debug mode).
  • Build KLEE (from the KLEE source directory):
    - make + make ENABLE_OPTIMIZED=1
  • -
  • Run DejaGNU and unit tests to verify your build: +
  • Run the regression suite to verify your build:
    make check
    make unittests
    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; } + You can find the entire code for this example here.

    Marking input as symbolic

    @@ -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 replay driver, which simply replaces + provides a convenient replay library, which simply replaces the call to klee_make_symbolic 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 libkleeRuntest + library and set the KLEE_RUNTEST environment variable to + point to the name of the desired test case:
    -  $ gcc ... 
    + $ 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 + + As expected, our program returns 1 when running the first test case + (which contains the lowercase letter 'b'), and 0 when + running the other two (which don't contain lowercase letters). + +

    -
    -- cgit 1.4.1