Changed bout to ktest. Kept "BOUT\n" as the header of test files, for backward compatibility. Also changed KLEE_RUNTEST to KTEST_FILE. Updated tutorial-1.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72312 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 19 insertions, 17 deletions

diff --git a/www/tutorial-1.html b/www/tutorial-1.html
index 389359b2..9f458237 100644
--- a/www/tutorial-1.html
+++ b/www/tutorial-1.html
@@ -101,33 +101,34 @@
 
   <pre class="output">
   $ ls klee-last/
-  assembly.ll  messages.txt  run.stats        test000002.bout  warnings.txt 
-  info         run.istats    test000001.bout  test000003.bout  </pre>
+  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>.bout</tt>.  These are
-  binary files, which can be read with the <tt>klee-bout-tool</tt>
+  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">
-  $ klee-bout-tool klee-last/test000001.bout 
-  bout file  : 'klee-last/test000001.bout'
+  $ ktest-tool klee-last/test000001.ktest 
+  bout file  : 'klee-last/test000001.ktest'
   args       : ['demo.o']
   num objects: 1
   object    0: name: 'input'
   object    0: size: 1
-  object    0: data: 'b' 
+  object    0: data: 'b'
 
-  $ klee-bout-tool klee-last/test000002.bout 
+  $ ktest-tool klee-last/test000002.ktest 
   ...
   object    0: data: '~'
- 
-  $ klee-bout-tool klee-last/test000003.bout 
-  ...
+
+  $ ktest-tool klee-last/test000003.ktest 
+  ..
   object    0: data: '\x00' </pre>
 
   In each test file, KLEE reports the arguments with which the program
@@ -150,21 +151,22 @@
   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 .bout file.
+  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>KLEE_RUNTEST</tt> environment variable to
+  library and set the <tt>KTEST_FILE</tt> environment variable to
   point to the name of the desired test case:
 
   <pre class="output">
-  $ gcc path/to/klee/Release/lib/libkleeRuntest.dylib demo.c
-  $ KLEE_RUNTEST=klee-last/test000001.bout ./a.out 
+  $ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
+  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
   $ echo $?
   1
-  $ KLEE_RUNTEST=klee-last/test000002.bout ./a.out 
+  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
   $ echo $?
   0
-  $ KLEE_RUNTEST=klee-last/test000003.bout ./a.out
+  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
   $ echo $?
   0 </pre>