diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2012-10-24 15:09:59 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2012-10-24 15:09:59 +0000 |
| commit | a45a0b93894bcc7a3c164934c33595a98693f54c (patch) | |
| tree | 7226139fbd606e4624507cc01ba66af4b9120357 | |
| parent | e8c6be312a3e74f158fe11ff3e67f70189a167de (diff) | |
| download | klee-a45a0b93894bcc7a3c164934c33595a98693f54c.tar.gz | |
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
| -rw-r--r-- | www/klee-files.html | 30 |
1 files changed, 29 insertions, 1 deletions
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 @@ <h2>Other Global Files</h2> <ol> - <li><b>queries.pc:</b> </li> + <li><b>all-queries.pc:</b> This file contains all the queries KLEE + made during execution in the <a href="KQuery.html">KQuery</a> + 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 <tt>--use-query-log=all:pc</tt> to KLEE.</li> + <li><b>all-queries.smt2:</b> This file contains all the queries KLEE made during execution in the <a href="http://www.smtlib.org">SMT-LIBv2</a> + .It contains the same information as <tt>all-queries.pc</tt>. + The generation of this file can be enabled by specifying the option <tt>--use-query-log=all:smt2</tt> to KLEE.</li> + <li><b>solver-queries.pc:</b> This file contains all the queries passed to KLEE's underlying solver during execution in the + <a href="KQuery.html">KQuery</a> 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 <tt>--use-query-log=solver:pc</tt> to KLEE.</li> + <li><b>solver-queries.smt2:</b> This file contains all the queries passed to KLEE's underlying solver during execution in the + <a href="http://www.smtlib.org">SMT-LIBv2</a> + format. It contains the same information as <tt>solver-queries.pc</tt>. + The generation of this file can be enabled by specifying the option <tt>--use-query-log=solver:smt2</tt> to KLEE.</li> </ol> @@ -101,6 +121,14 @@ the <tt>--write-pcs</tt> flag. (This is the same information as in the corresponding <tt>.pc</tt> file.) </li> + <li> + <b>test<N>.smt2:</b> Contains the constraints associated + with the given path, + in <a href="http://www.smtlib.org/">SMT-LIBv2</a> + format. The generation of these files can be enabled via + the <tt>--write-smt2s</tt> flag. (This is the same information as + in the corresponding <tt>.pc</tt> file.) + </li> </ol> |