KLEE生成的主要文件清单

• 文献标题： Overview of the main files generated by KLEE
• 文献作者： The KLEE Team.
• 文献来源： http://klee.github.io/docs/files/
• 阅读日期： 2015年12月23日22时许
• 阅读程度： 速读

标准全局文件

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
2. warnings.txt： 包含了KLEE生成的所有警告信息的文本文件。
3. messages.txt： 包含了KLEE生成的所有消息的文本文件。
4. assembly.ll： 包含了被KLEE执行的可读样式的LLVM bitcode。
5. run.stats： 包含了KLEE生成的各式统计信息的文本文件，可以用klee-stats工具解析它。
6. run.istats： 包含KLEE生成的程序中每行代码对应的全局统计信息的二进制文件。

其他全局文件

1. all-queries.pc： KLEE在KQuery模式下执行的所有查询。这些是优化之前的查询，所以有些记录的查询可能根本没被KLEE求解器修改或执行。文件输出开关为：--use-query-log=all:pc to KLEE.
2. all-queries.smt2： 包含在SMT-LIBv2中的执行的KLEE查询。包含的信息同文件all-queries.pc.开关参数为： --use-query-log=all:smt2 to KLEE.
3. solver-queries.pc： 包含KQuery格式下所有传递给KLEE求解器的查询，这些查询是优化后的。开关参数为：--use-query-log=solver:pc to KLEE.
4. solver-queries.smt2： 包含SMT-LIBv2格式下所有传递给KLEE求解器的查询，这些查询是优化后的。包含的信息同文件solver-queries.pc。开关参数为：--use-query-log=solver:smt2 to KLEE.

路径相关文件

1. test<N>.ktest： KLEE生成的能触发该路径的测试样本，要用ktest-tool处理该文件。可以用 --no-output 参数关闭此文件的生成。
2. test<N>.<error-type>.err： 当KLEE在触发路径时出错，生成此文件，包含了文本样式的错误信息。
3. test<N>.pc： 以KQuery格式存储与该路径相关的约束。通过 --write-pcs 开关生成此类文件。
4. test<N>.cvc： 以CVC格式存储与该路径相关的约束。通过 --write-cvcs 开关生成此类文件。
5. test<N>.smt2： 以SMT-LIBv2格式存储与该路径相关的约束。通过 --write-smt2s 开关生成此类文件。