Contents

• Standard Global Files
• Other Global Files
• Per-path files

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 command-line with which KLEE was run, and the total time taken by the execution, e.g.:

   $ cat info
   klee --write-kqueries 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 queries = 3
   KLEE: done: query cex = 3
   KLEE: done: total instructions = 67
   KLEE: done: completed paths = 3
   KLEE: done: generated tests = 3
   

2. warnings.txt: This is a text file containing all warnings emitted by KLEE.
3. messages.txt: This is a text file containing all other messages emitted by KLEE.
4. assembly.ll: This file contains a human readable version of the LLVM bitcode executed by KLEE
5. run.stats: This is a SQLite file containing various statistics emitted by KLEE. While this file can be inspected manually, you should use the klee-stats tool for that.
6. run.istats: This is a binary file containing global statistics emitted by KLEE for each line of code in the program.

Other Global Files

1. all-queries.kquery: 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:kquery to KLEE.
2. 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.kquery. The generation of this file can be enabled by specifying the option --use-query-log=all:smt2 to KLEE.
3. solver-queries.kquery: 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:kquery to KLEE.
4. 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.kquery. The generation of this file can be enabled by specifying the option --use-query-log=solver:smt2 to KLEE.

Per-path files

1. 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 --write-no-tests option.
2. test<N>.<error-type>.err: Generated for paths where KLEE found an error. Contains information about the error in textual form.
3. test<N>.kquery: Contains the constraints associated with the given path, in KQuery format. The generation of these files can be enabled via the --write-kqueries flag.
4. 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-cvcs flag. (This is the same information as in the corresponding .kquery file.)
5. 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 .kquery file.)