From 69c4c5548d5e366113b376d77520df7f79142403 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 21 May 2009 06:59:38 +0000 Subject: Started web pages describing the main KLEE tools, and the main files generated by KLEE. Small updates to the CSS file and tutorials.html git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72208 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/klee-files.html | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 www/klee-files.html (limited to 'www/klee-files.html') diff --git a/www/klee-files.html b/www/klee-files.html new file mode 100644 index 00000000..a15b0c0b --- /dev/null +++ b/www/klee-files.html @@ -0,0 +1,78 @@ + + + + + + The KLEE Symbolic Virtual Machine + + + + + +
+ +

KLEE Generated Files

+ + +

Standard Files

+ These 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 + command-line with which KLEE was run, and the total time taken by + the execution. E.g.: + 
    +    $ cat info 
+    klee --write-pcs demo.o
+    PID: 12460
+    Started: 2009-05-20 22:31:41
+    BEGIN searcher description
+    DFSSearcher
+    END searcher description
+    Finished: 2009-05-20 22:31:41
+    Elapsed: 00:00:00
+    KLEE: done: explored paths = 3
+    KLEE: done: avg. constructs per query = 6
+    KLEE: done: total queries = 3
+    KLEE: done: valid queries = 0
+    KLEE: done: invalid queriers = 3
+    KLEE: done: query cex = 3
+    KLEE: done: total instructions = 67
+    KLEE: done: completed paths = 3
+    KLEE: done: generated tests = 3
    +
    2. + +
  2. warnings.txt: This is a text file containing all warnings emitted by KLEE. +
    3. + +
  3. messages.txt: This is a text file containing all other messages emitted by KLEE. +
    4. + +
  4. assembly.ll: This file contains a human readable version + of the LLVM bitcode executed by KLEE + +
  5. 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 + tool for that.
    6. + +
  6. run.istats: This is a binary file containing global + statistics emitted by KLEE for each line of code in the program. +
    7. + +
+ + +

Kleaver files

+ +
    +
  1. test<NNN>.pc files: +
    2. +
  2. queries.pc: +
    3. +
+ +
+ + -- cgit 1.4.1