about summary refs log tree commit diff homepage
path: root/www/Tutorial-1.html
diff options
context:
space:
mode:
authorDominic Chen <d.c.ddcc@gmail.com>2013-07-25 10:45:32 +0100
committerDominic Chen <d.c.ddcc@gmail.com>2013-07-25 10:45:32 +0100
commit6ae711b1d900bffbca407fe97d5e5ce97745dff1 (patch)
treeda6a64772f9440601c7b0efd816b06c40bdf90d8 /www/Tutorial-1.html
parent7d76de96751796cca076e021575fafd459eef6fb (diff)
downloadklee-6ae711b1d900bffbca407fe97d5e5ce97745dff1.tar.gz
move website to separate repo
Diffstat (limited to 'www/Tutorial-1.html')
-rw-r--r--www/Tutorial-1.html187


1 files changed, 0 insertions, 187 deletions
diff --git a/www/Tutorial-1.html b/www/Tutorial-1.html
deleted file mode 100644
index 38c3b101..00000000
--- a/www/Tutorial-1.html
+++ /dev/null
@@ -1,187 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" 
-          "http://www.w3.org/TR/html4/strict.dtd">
-<!-- Material used from: HTML 4.01 specs: http://www.w3.org/TR/html401/ -->
-<html>
-<head>
-  <META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
-  <title>KLEE - Tutorial One</title>
-  <link type="text/css" rel="stylesheet" href="menu.css">
-  <link type="text/css" rel="stylesheet" href="content.css">
-</head>
-<body>
-<!--#include virtual="menu.html.incl"-->
-<div id="content">
-  <!--*********************************************************************-->
-  <h1>Tutorial One: Testing a Small Function</h1>
-  <!--*********************************************************************-->
-  
-  <h2>The demo code</h2>
-
-  This tutorial walks you through the main steps needed to test a
-  simple function with KLEE.  Here is our simple function:
-
-  <pre class="code">
-  int get_sign(int x) {
-    if (x == 0)
-       return 0;
-
-    if (x < 0)
-       return -1;
-    else 
-       return 1;
-  } </pre>
-
-  You can find the entire code for this example in the source tree
-  under <tt>examples/get_sign</tt>.  A version of the source code can
-  also be accessed <a href="resources/get_sign.c.html">here</a>. 
-
-  <h2>Marking input as symbolic</h2> 
-
-  In order to test this function with KLEE, we need to run it
-  on <i>symbolic</i> input.  To mark a variable as symbolic, we use
-  the <tt>klee_make_symbolic()</tt> function, which takes three
-  arguments: the address of the variable (memory location) that we
-  want to treat as symbolic, its size, and a name (which can be
-  anything).  Here is a simple <tt>main()</tt> function that marks a
-  variable <tt>a</tt> as symbolic and uses it to
-  call <tt>get_sign()</tt>:
-
-  <pre class="code">
-  int main() {
-      int a;
-      klee_make_symbolic(&a, sizeof(a), "a");
-      return get_sign(a);
-  } </pre>
-		
-
-
-  <h2>Compiling to LLVM bitcode</h2>
-
-  KLEE operates on LLVM bitcode.  To run a program with KLEE, you
-  first compile it to LLVM bitcode using <tt>llvm-gcc
-  --emit-llvm</tt>.  Assuming our code is stored in <tt>get_sign.c</tt>,
-  we run:
-
-  <div class="instr">
-  llvm-gcc --emit-llvm -c -g get_sign.c
-  </div>
-
-  to generate the LLVM bitcode file <tt>get_sign.o</tt>.
-
-  It is useful to (1) build with <tt>-g</tt> to add debug information
-  to the bitcode file, which we use to generate source line level
-  statistics information, and (2) not use any optimization flags.  The
-  code can be optimized later, as KLEE provides the
-  <tt>--optimize</tt> command line option to run the optimizer
-  internally.
-    
-  <h2>Running KLEE</h2>
-      
-  To run KLEE on the bitcode file simply execute:
-  
-  <div class="instr">
-  klee get_sign.o
-  </div>
-
-  You should see the following output (assumes LLVM 2.8):
-  <pre class="output">
-  KLEE: output directory = "klee-out-0"
-
-  KLEE: done: total instructions = 51
-  KLEE: done: completed paths = 3
-  KLEE: done: generated tests = 3 </pre>
-
-  There are three paths through our simple function, one
-  where <tt>a</tt> is <tt>0</tt>, one where it is less than <tt>0</tt>
-  and one where it is greater than <tt>0</tt>.
-
-  As expected, KLEE informs us that it explored three paths in the
-  program and generated one test case for each path explored.  The
-  output of a KLEE execution is a directory (in our
-  case <tt>klee-out-0</tt>) containing the test cases generated by
-  KLEE.  KLEE names the output directory <tt>klee-out-N</tt> where N
-  is the lowest available number (so if we run KLEE again it will
-  create a directory called <tt>klee-out-1</tt>), and also generates a
-  symbolic link called <tt>klee-last</tt> to this directory for
-  convenience:
-
-  <pre class="output">
-  $ ls klee-last/
-  assembly.ll      run.istats       test000002.ktest
-  info             run.stats        test000003.ktest
-  messages.txt     test000001.ktest warnings.txt </pre>
-
-  Please click <a href="klee-files.html">here</a> if you would like an
-  overview of the files generated by KLEE.  In this tutorial, we only
-  focus on the actual test files generated by KLEE.
-
-  <h2>KLEE-generated test cases</h2> The test cases generated by KLEE
-  are written in files with extension <tt>.ktest</tt>.  These are
-  binary files, which can be read with the <tt>ktest-tool</tt>
-  utility.  So let's examine each file:
-
-  <pre class="output">
-  $ ktest-tool --write-ints klee-last/test000001.ktest 
-  ktest file : 'klee-last/test000001.ktest'
-  args       : ['get_sign.o']
-  num objects: 1
-  object    0: name: 'a'
-  object    0: size: 4
-  object    0: data: 1
-  
-  $ ktest-tool --write-ints klee-last/test000002.ktest  
-  ...
-  object    0: data: -2147483648
-
-  $ ktest-tool --write-ints klee-last/test000003.ktest 
-  ...
-  object    0: data: 0 </pre>
-
-  In each test file, KLEE reports the arguments with which the program
-  was invoked (in our case no arguments other than the program name
-  itself), the number of symbolic objects on that path (only one in
-  our case), the name of our symbolic object ('a') and its size (4).
-  The actual test itself is represented by the value of our
-  input: <tt>1</tt> for the first test, <tt>-2147483648</tt> for the
-  second and <tt>0</tt> for the last one.  As expected, KLEE generated
-  value <tt>0</tt>, one negative value (<tt>-2147483648</tt>), and one
-  positive value (<tt>1</tt>).  We can now run these values on a
-  native version of our program, to exercise all paths through the
-  code!
- 
-
-  <h2>Replaying a test case</h2> 
-
-  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 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 <tt>.ktest</tt>
-  file.
-
-  To use it, simply link your program with the <tt>libkleeRuntest</tt>
-  library and set the <tt>KTEST_FILE</tt> environment variable to
-  point to the name of the desired test case:
-
-  <pre class="output">
-  $ export LD_LIBRARY_PATH=path-to-klee-root/Release+Asserts/lib/:$LD_LIBRARY_PATH
-  $ gcc -L path-to-klee-root/Release+Asserts/lib/ get_sign.c -lkleeRuntest
-  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
-  $ echo $?
-  1
-  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
-  $ echo $?
-  255
-  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
-  $ echo $?
-  0 </pre>
-
-  As expected, our program returns 1 when running the first test case,
-  255 (-1 converted to a valid exit code value in the 0-255 range)
-  when running the second one, and 0 when running the last one.
-
-  <br/><br/>
-
-</div>
-</body>
-</html>

 

generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-03-02 11:00:35 +0000