From 992bb82423849797546804da1f73e970fc748928 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 20 Jun 2012 18:31:40 +0000 Subject: 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 --- www/Tutorial-1.html | 4 ++-- www/klee-files.html | 45 ++++++++++++++++++++++++++++++++++++++------- 2 files changed, 40 insertions(+), 9 deletions(-) (limited to 'www') 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 @@ } You can find the entire code for this example in the source tree - under examples/islower. A version of the source code can + under examples/get_sign. A version of the source code can also be accessed here.

Marking input as symbolic

@@ -164,7 +164,7 @@ point to the name of the desired test case: 
-  $ 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 @@
 
 

   
-  
KLEE Generated Files

+  
Files generated by KLEE

   
 
-  
Standard Files

-  These files are always generated on a KLEE execution:
+  
Standard Global Files
 
+
+  These are global files are always generated on a KLEE execution:
   
    
   
  1. info: This is a text file containing various information
   related to a KLEE run.  In particular, it records the exact
@@ -54,25 +55,55 @@
 
   
  2. run.stats: This is a text file containing various
   statistics emitted by KLEE.  While this file can be inspected
-  manually, you should use the klee-stats
+  manually, you should use the klee-stats
   tool for that.
    3. 
 
   
  3. run.istats: This is a binary file containing global
   statistics emitted by KLEE for each line of code in the program.
   
    4. 
+
+  

+
   
+  
Other Global Files

+
+  
    
+    
  1. queries.pc:  
    2. 
   

 
 
-  
 Kleaver files

+  
 Per-path files

 
   
    
-    
  1. test<NNN>.pc files:
+    
  2. 
+      test<N>.ktest: Contains the test case generated by
+      KLEE on that path.  Use ktest-tool
+      to read the contents.  The generation of .ktest files
+      can be disabled using the --no-output option.
     
    3. 
-    
  3. queries.pc:
+
+    
  4. 
+      test<N>.<error-type>.err: Generated for paths
+      where KLEE found an error.  Contains information about the error
+      in textual form.
+    
    5. 
+
+    
  5. test<N>.pc: Contains the constraints associated with the given
+    path, in KQuery format.  The generation
+    of these files can be enabled via the --write-cvcs flag.
+    
    6. 
+
+    
  6. 
+      test<N>.cvc: Contains the constraints associated
+    with the given path,
+    in CVC
+    format.  The generation of these files can be enabled via
+    the --write-pcs flag.  (This is the same information as
+    in the corresponding .pc file.)
     
    7. 
   

 
+
 

 
 
-- 
cgit 1.4.1