【KLEE执行时生成的标准全局文件】
1 KLEE执行时总会生成的文件
1.1 info
info是一个txt文件，它包含与KLEE运行相关的信息。具体地，它记录运行KLEE的命令行语句及其执行的总体时间。
1.2 warnings.txt
warnings.txt是一个txt文件，它包含KLEE生成的警告信息。
1.3 messages.txt
messages.txt是一个txt文件，它包含KLEE生成的其它信息。
1.4 assembly.ll
assembly.ll是由KLEE执行的LLVM bitcode的人类可读的版本。
1.5 run.stats
run.stats是一个SQLite文件，它包含KLEE生成的各种数据。用户可以使用‘klee-stats’工具来查看此文件。
1.6 run.istats
run.istats是一个二进制文件，它包含KLEE针对程序中的每行代码生成的全局数据。
2 KLEE执行时生成的其它全局文件
2.1 all-queries.kquery
all-queries.kquery包含KLEE执行期间所做的所有查询，它以KQuery的形式呈现。这些查询是在优化（包括缓存、约束依赖）前生成的，故有些查询可能从未被KLEE求解器执行或者在KLEE求解器执行前已被更改。KLEE的命令行中指定‘–use-query-log=all:kquery’选项可生成此文件。
2.2 all-queries.smt2
all-queries.smt2包含KLEE执行期间所做的所有查询，它以SMT-LIBv2的形式呈现。其内容与all-queries.kquery相同。KLEE的命令行中指定‘–use-query-log=all:smt2’选项可生成此文件。
2.3 solver-queries.kquery
solver-queries.kquery包含KLEE执行期间传递给KLEE求解器的查询，它以KQuery的形式呈现。这些查询是在优化（包括缓存、约束依赖）后生成的。KLEE的命令行中指定‘–use-query-log=solver:kquery’选项可生成此文件。
2.4 solver-queries.smt2
solver-queries.smt2包含KLEE执行期间传递给KLEE求解器的查询，它以SMT-LIBv2的形式呈现。其内容与solver-queries.kquery相同。KLEE的命令行中指定‘–use-query-log=solver:smt2’选项可生成此文件。
3 每条路径文件
3.1 test<N>.ktest
test.ktest包含KLEE在每条路径上生成的测试用例。可以使用’ktest-tool‘来阅读此文件。使用’–no-output‘选项可禁用.ktest文件。N对应路径数量。
3.2 test<N>.<error-type>.err
test..err为KLEE发现错误的路径生成，它以文本形式包含有关错误的信息。
3.3 test<N>.kquery
test.kquery包含与给定路径相关的约束，它以KQuery的形式呈现。KLEE的命令行中指定‘–write-kqueries’选项可生成此文件。
3.4 test<N>.cvc
test.cvc包含与给定路径相关的约束，它以CVC的形式呈现。其内容与.kquery相同。KLEE的命令行中指定‘ --write-cvcs’选项可生成此文件。
3.5 test<N>.smt2
test.smt2包含与给定路径相关的约束，它以SMT-LIBv2的形式呈现。内容与.kquery相同。KLEE的命令行中指定‘ --write-smt2s’选项可生成此文件。
至此，KLEE执行时生成的标准全局文件已叙述完毕。