Web page updates: (1) Improved documentation on files generated by

KLEE; (2) Fixed a couple of errors in Tutorial One, pointed out by
Hristina Palikareva.



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

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&lt;NNN&gt;.pc</b> files:
+    <li>
+      <b>test&lt;N&gt;.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&lt;N&gt;.&lt;error-type&gt;.err</b>: Generated for paths
+      where KLEE found an error.  Contains information about the error
+      in textual form.
+    </li>
+
+    <li><b>test&lt;N&gt;.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&lt;N&gt;.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>