From a45a0b93894bcc7a3c164934c33595a98693f54c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 24 Oct 2012 15:09:59 +0000 Subject: Patch by Dan Liew, updating klee-files.html to mention the recently added SMTLIB options. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166570 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/klee-files.html | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/www/klee-files.html b/www/klee-files.html index 73ca3535..299f593b 100644 --- a/www/klee-files.html +++ b/www/klee-files.html @@ -68,7 +68,27 @@

Other Global Files

    -
  1. queries.pc:
    2. +
  2. all-queries.pc: This file contains all the queries KLEE + made during execution in the KQuery + format. Note these are the queries before any optimisation + (e.g. caching, constraint independence) so it is possible that + some of the queries logged are never executed by KLEE's underlying + solver or are modified before being executed by KLEE's underlying + solver. The generation of this file can be enabled by specifying + the option --use-query-log=all:pc to KLEE.
    3. +
  3. all-queries.smt2: This file contains all the queries KLEE made during execution in the SMT-LIBv2 + .It contains the same information as all-queries.pc. + The generation of this file can be enabled by specifying the option --use-query-log=all:smt2 to KLEE.
    4. +
  4. solver-queries.pc: This file contains all the queries passed to KLEE's underlying solver during execution in the + KQuery format. Note these are the + queries after all optimisations (e.g. caching, constraint + independence) are performed. The generation of this file can be + enabled by specifying the + option --use-query-log=solver:pc to KLEE.
    5. +
  5. solver-queries.smt2: This file contains all the queries passed to KLEE's underlying solver during execution in the + SMT-LIBv2 + format. It contains the same information as solver-queries.pc. + The generation of this file can be enabled by specifying the option --use-query-log=solver:smt2 to KLEE.
@@ -101,6 +121,14 @@ the --write-pcs flag. (This is the same information as in the corresponding .pc file.) +
  • + test<N>.smt2: Contains the constraints associated + with the given path, + in SMT-LIBv2 + format. The generation of these files can be enabled via + the --write-smt2s flag. (This is the same information as + in the corresponding .pc file.) +
    • -- cgit 1.4.1