1 Standard Global Files
有些文件在KLEE执行过程中总是会生成，这些称为是Global files
1-1 info文件：该文本文件存储了KLEE运行产生的各类相关信息，其中记录了命令行的命令、总的运行时间等等信息，具体例如下（都是很直观的描述，比较容易懂）：
$ 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
1-2 warnings.txt: 记录相关警告信息.
1-3 messages.txt: 包含了一些被KLEE忽略的消息.
1-4 assembly.ll: 这里是人可读的编译代码，LLVM可以生成
1-5 run.stats: 这里存储了KLEE输出中省略掉的一些统计信息，可以用klee-stats工具来读取该文件.
1-6 run.istats: 该二进制文件包含全局统计信息，具体详细到了程序的各行代码.
2 Other Global Files （具体有些我也没有看过，后面看了有体会了再补充这里，也不懂各种查询干什么用）
2-1 all-queries.pc: 记录了在KLEE执行期间做的一些查询，格式为KQuery。为了生成该文件，需要在运行时增加参数设定：--use-query-log=all:pc。
2-2 all-queries.smt2: 以SMT-LIBv2格式记录了一些查询，包含的信息与all-queries.pc同。为了生成该文件，需要在运行时增加参数设定：--use-query-log=all:smt2 to KLEE。
2-3 solver-queries.pc: 记录提交给KLEE’s underlying solver的查询，格式为KQuery 。为了生成该文件，需要在运行时增加参数设定：--use-query-log=solver:pc to KLEE.
2-4 solver-queries.smt2: 这里记录的是提交给KLEE’s underlying solver的查询，格式为SMT-LIBv2。为了生成该文件，需要在运行时增加参数设定：--use-query-log=solver:smt2 to KLEE.
3 Per-path files
3-1 test<N>.ktest: 包含在KLEE执行路径中生成的测试例，可以使用ktest-tool读取相关内容，如果不要输出相关文件，可以再运行参数上设置 --no-output option.
3-2 test<N>.<error-type>.err: 产生KLEE路径的错误信息，格式为文本.
3-3 test<N>.pc: 包含于特定路径相关的约束信息，格式为KQuery，要设定是否输出该部分信息，可以通过设置参数 --write-cvcs.
3-4 test<N>.cvc: 包含与特定path相关的约束信息，格式为CVC，要设定是否输出该部分信息，可以通过设置参数--write-pcs flag.
3-5 test<N>.smt2: 包含与特定path相关的约束信息，格式为SMT-LIBv2，要设定是否输出该部分信息，可以通过设置参数--write-smt2s flag.