diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2013-01-06 16:37:11 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2013-01-06 16:37:11 +0000 |
| commit | 4f1d842f3b13cbdcbc44065a51365931e5ce8fe0 (patch) | |
| tree | 74f5c5b9d6650fafedc6aac030383d15760e5227 /www | |
| parent | 6f33a34d779489590e80415e13dfacab035c2364 (diff) | |
| download | klee-4f1d842f3b13cbdcbc44065a51365931e5ce8fe0.tar.gz | |
Some documentation on query logging.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171657 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'www')
| -rw-r--r-- | www/Documentation.html | 2 | ||||
| -rw-r--r-- | www/klee-options.html | 30 |
2 files changed, 29 insertions, 3 deletions
diff --git a/www/Documentation.html b/www/Documentation.html index b266e439..11152801 100644 --- a/www/Documentation.html +++ b/www/Documentation.html @@ -24,7 +24,7 @@ <li> <a href="klee-options.html">KLEE Options</a>: - Overview of the KLEE's main command-line options. + Overview of KLEE's main command-line options. </li> <li> diff --git a/www/klee-options.html b/www/klee-options.html index 22871e0e..be997ec4 100644 --- a/www/klee-options.html +++ b/www/klee-options.html @@ -15,7 +15,12 @@ <h1>KLEE Options</h1> <!--*********************************************************************--> - <h2>Search Heuristics</h2> + <h3> + <a href="#search"> 1. Search Heuristics</a> <br/> + <a href="#logging"> 2. Query Logging</a> <br/> + </h3> + + <h2 id="search">Search Heuristics</h2> <h3>Main search heuristics</h3> @@ -67,7 +72,28 @@ <p> The default heuristics used by KLEE are <i>random-path</i> interleaved with <i>nurs:covnew</i>. </p> - + + <h2 id="logging">Query Logging</h2> + + To log the queries issued by KLEE during symbolic execution, you can use the following options: + <ol> + <li> + <b>--use-query-log=TYPE:FORMAT</b>, where: + <ul> + <li><b>TYPE</b> is either <b>all</b> to log all the queries KLEE made during execution before any optimisation (e.g. caching, constraint independence) is performed, or <b>solver</b> to log only the queries passed to KLEE's underlying solver. Note that it is possible that some of the unoptimized queries are never executed or are modified before being executed by KLEE's underlying solver.</li> + <li><b>FORMAT</b> is the format in which queries are logged and can be either <b>pc</b> for the <a href="KQuery.html">KQuery</a> format, or <b>smt2</b> for the <a href="http://www.smtlib.org">SMT-LIBv2</a> format. + </ul> + <li> + <b>--min-query-time-to-log=TIME</b> (in ms) is used to log only queries that exceed a certain time limit. <b>TIME</b> can be: + <ul> + <li><b>0</b> (default): to log all queries</li> + <li><b><0</b>: a negative value specifies that only queries that timed out should be logged. The timeout value is specified via the <b>--max-stp-time</b> option.</li> + <li><b>>0</b>: only queries that took more that <b>TIME</b> milliseconds should be logged. + </ul> + </li> + </li> + </ol> + </div> </body> </html> |