- 文献标题： Overview of the main files generated by KLEE
- 文献作者： The KLEE Team.
- 文献来源： http://klee.github.io/docs/files/
- 阅读日期： 2015年12月23日22时许
- 阅读程度： 速读
标准全局文件
-
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 - warnings.txt： 包含了KLEE生成的所有警告信息的文本文件。
- messages.txt： 包含了KLEE生成的所有消息的文本文件。
- assembly.ll： 包含了被KLEE执行的可读样式的LLVM bitcode。
- run.stats： 包含了KLEE生成的各式统计信息的文本文件，可以用klee-stats工具解析它。
- run.istats： 包含KLEE生成的程序中每行代码对应的全局统计信息的二进制文件。
其他全局文件
- all-queries.pc： KLEE在KQuery模式下执行的所有查询。这些是优化之前的查询，所以有些记录的查询可能根本没被KLEE求解器修改或执行。文件输出开关为：--use-query-log=all:pc to KLEE.
- all-queries.smt2： 包含在SMT-LIBv2中的执行的KLEE查询。包含的信息同文件all-queries.pc.开关参数为： --use-query-log=all:smt2 to KLEE.
- solver-queries.pc： 包含KQuery格式下所有传递给KLEE求解器的查询，这些查询是优化后的。开关参数为：--use-query-log=solver:pc to KLEE.
- solver-queries.smt2： 包含SMT-LIBv2格式下所有传递给KLEE求解器的查询，这些查询是优化后的。包含的信息同文件solver-queries.pc。开关参数为：--use-query-log=solver:smt2 to KLEE.
路径相关文件
- test<N>.ktest： KLEE生成的能触发该路径的测试样本，要用ktest-tool处理该文件。可以用 --no-output 参数关闭此文件的生成。
- test<N>.<error-type>.err： 当KLEE在触发路径时出错，生成此文件，包含了文本样式的错误信息。
- test<N>.pc： 以KQuery格式存储与该路径相关的约束。通过 --write-pcs 开关生成此类文件。
- test<N>.cvc： 以CVC格式存储与该路径相关的约束。通过 --write-cvcs 开关生成此类文件。
- test<N>.smt2： 以SMT-LIBv2格式存储与该路径相关的约束。通过 --write-smt2s 开关生成此类文件。
