diff options
Diffstat (limited to 'www/tutorial-1.html')
| -rw-r--r-- | www/tutorial-1.html | 36 |
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> |