diff options
| -rw-r--r-- | www/Tutorial-1.html | 4 | ||||
| -rw-r--r-- | www/klee-files.html | 45 |
2 files changed, 40 insertions, 9 deletions
diff --git a/www/Tutorial-1.html b/www/Tutorial-1.html index 49d0c7de..beb306e6 100644 --- a/www/Tutorial-1.html +++ b/www/Tutorial-1.html @@ -32,7 +32,7 @@ } </pre> You can find the entire code for this example in the source tree - under <tt>examples/islower</tt>. A version of the source code can + 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> @@ -164,7 +164,7 @@ point to the name of the desired test case: <pre class="output"> - $ gcc ~klee/Release+Asserts/lib/libkleeRuntest.so get_sign.c + $ gcc path-to-klee-root/Release+Asserts/lib/libkleeRuntest.so get_sign.c $ KTEST_FILE=klee-last/test000001.ktest ./a.out $ echo $? 1 diff --git a/www/klee-files.html b/www/klee-files.html index a15b0c0b..73ca3535 100644 --- a/www/klee-files.html +++ b/www/klee-files.html @@ -12,11 +12,12 @@ <!--#include virtual="menu.html.incl"--> <div id="content"> <!--*********************************************************************--> - <h1>KLEE Generated Files</h1> + <h1>Files generated by KLEE</h1> <!--*********************************************************************--> - <h2>Standard Files</h2> - These files are always generated on a KLEE execution: + <h2>Standard Global Files</h2> + + These are global files are always generated on a KLEE execution: <ol> <li><b>info</b>: This is a text file containing various information related to a KLEE run. In particular, it records the exact @@ -54,25 +55,55 @@ <li><b>run.stats</b>: This is a text file containing various statistics emitted by KLEE. While this file can be inspected - manually, you should use the <a href="klee-tools">klee-stats</a> + manually, you should use the <a href="klee-tools.html">klee-stats</a> tool for that.</li> <li><b>run.istats</b>: This is a binary file containing global statistics emitted by KLEE for each line of code in the program. </li> + + </ol> + + <h2>Other Global Files</h2> + + <ol> + <li><b>queries.pc:</b> </li> </ol> - <h2> Kleaver files</h2> + <h2> Per-path files</h2> <ol> - <li><b>test<NNN>.pc</b> files: + <li> + <b>test<N>.ktest</b>: Contains the test case generated by + KLEE on that path. Use <a href="klee-tools.html">ktest-tool</a> + to read the contents. The generation of <tt>.ktest</tt> files + can be disabled using the <tt>--no-output</tt> option. </li> - <li><b>queries.pc:</b> + + <li> + <b>test<N>.<error-type>.err</b>: Generated for paths + where KLEE found an error. Contains information about the error + in textual form. + </li> + + <li><b>test<N>.pc:</b> Contains the constraints associated with the given + path, in <a href="KQuery.html">KQuery</a> format. The generation + of these files can be enabled via the <tt>--write-cvcs</tt> flag. + </li> + + <li> + <b>test<N>.cvc:</b> Contains the constraints associated + with the given path, + in <a href="https://sites.google.com/site/stpfastprover/stp-documentation#TOC-The-CVC-language">CVC</a> + format. The generation of these files can be enabled via + the <tt>--write-pcs</tt> flag. (This is the same information as + in the corresponding <tt>.pc</tt> file.) </li> </ol> + </div> </body> </html> |