KLEE生成的文件
Sun, May 1, 2016 · #翻译 #学习 Tags: KLEE基础全局文件
| 文件名 | 描述 |
|---|---|
| info | 记录klee运行的各种相关信息，如使用的命令，运行时间等 |
| warnings.txt | KLEE运行过程中生成的warning信息 |
| messages.txt | KLEE运行过程中生成的其他messages |
| assembly.ll | 将KLEE实际执行的LLVM bitcode转为可读的文本后的文件 |
| run.stats | KLEE生成的各种统计信息。能够人工查看，或使用klee-stats查看 |
| run.istats | KLEE生成的程序中每一行代码的全局统计信息global statistics |
其他全局文件（需要命令来指定生成）
| 文件名 | 描述 |
|---|---|
| all-queries.pc | 文件中以KQuery格式记录了KLEE在运行中产生的所有queries。 记录的queries没有经过任何优化（caching, constraint independence等），也就是说，其中有些queries从来没有被KLEE的求解器执行过，或者在执行前被修改了 需要的命令参数为 --use-query-log=all:pc |
| all-queries.smt2 | 文件中以SMT-LIBv2格式记录了KLEE在运行中产生的所有queries。 记录的内容与all-queries.pc含有相同的信息 需要的命令参数为 --use-query-log=all:smt2 |
| solver-queries.pc | 文件中以KQuery格式记录了运行过程中实际传给KLEE的underlying solver的所有queries。 记录的queries经过了所有的优化（caching, constraint independence等） 需要的命令参数为 --use-query-log=solver:pc |
| solver-queries.smt2 | 文件中以SMT-LIBv2格式记录了运行过程中实际传给KLEE的underlying solver的所有queries。 记录的内容与solver-queries.pc含有相同的信息 需要的命令参数为 --use-query-log=solver:smt2 |
每条路径的文件
| 文件名 | 描述 |
|---|---|
| test<N>.ktest | 文件内容为KLEE为这条路径生成的测试用例test case。可以使用ktest-tool查看内容。 可以使用命令参数 --no-output 禁用.ktest文件的输出 |
| test<N>.<error-type>.err | KLEE发现了错误error的路径将会产生这个文件。包含了这个error的信息。以文本形式储存 |
| test<N>.pc | 以KQuery格式记录，这个路径的约束。 使用命令参数 --write-pcs 来输出这个文件 |
| test<N>.cvc | 以CVC格式记录，这个路径的约束。 与对应的.pc文件包含相同的信息 使用命令参数 --write-cvcs 来输出这个文件 |
| test<N>.smt2 | 以SMT-LIBv2格式记录，这个路径的约束。 与对应的.pc文件包含相同的信息 使用命令参数 --write-smt2s 来输出这个文件 |