Files generated by KLEE

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-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. 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 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. 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. queries.pc:

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 --no-output 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>.pc: Contains the constraints associated with the given path, in KQuery format. The generation of these files can be enabled via the --write-cvcs 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-pcs flag. (This is the same information as in the corresponding .pc file.)