KLEE--KLEE主要的生成文件解读

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.

KLEE--KLEE主要的生成文件解读相关推荐

KLEE 使用（三）------ 使用 KLEE 为二分查找生成测试
在上一篇博文中,我们展示了如何用 KLEE 来为一个简单程序生成测试用例.在这篇博文中,我们将展示如何使用 KLEE 中的数组和断言. 0x1 测试无序数组如下是二分查找的算法实现: int bin ...
package.json文件解读
package.json文件解读 {"name": "vue-04-cli-demo1", // 项目名称 "version": " ...
STM32之CubeMX学习笔记（4）新建工程文件解读
文章目录芯片与板子介绍主频 RAM 与 Flash io数与封装内置外设板子外设新建工程文件的步骤选择芯片选取调试方式,选取高速晶振,调整时钟修改文件设置,和生成设置生成工程文件工 ...
node.js 生成文件_如何使用Node.js在几秒钟内生成模拟数据
node.js 生成文件介绍 (Introduction) In most of the applications, you need to have some static JSON data w ...
Android 源码编译及 mk文件解读
Android 源码编译参考:探索Android FrameWork底层开发视频_哔哩哔哩_bilibili 基础 1.源代码编译分为2个部分: (1)boot/Kernel (2)Android ...
PNG文件解读(2):PNG格式文件结构与数据结构解读—解码PNG数据
PNG文件识别之前写过<JPEG/Exif/TIFF格式解读(1):JEPG图片压缩与存储原理分析>,JPEG文件是以,FFD8开头,FFD9结尾,中间存储着以0xFFE0~0xFFEF ...
回调函数自定义传参_koroFileHeader：一个用于生成文件头部注释和函数注释的插件...
小金子读完需要 2分钟速读仅需 1 分钟大家好,我是你们的小金子. 今天给大家分享的这个工具呢?对于使用 VS Code 的同学来讲,是一个好东西. koroFileHeader,一个在 vsc ...
JAVA编译成文件的说法_下列关于使用Javac命令编译后生成文件的说法中，正确的是？...
下列关于使用Javac命令编译后生成文件的说法中,正确的是? 答:编译后生成的文件可以在Java虚拟机中运行\n\n编译后生成的文件为二进制文件\n\n编译后生成文件的后缀名为.class 线性表的链 ...
Delphi开发的数据库程序在C:\PDOXUSRS.NET生成文件，拒绝访问及读写权限
Delphi开发的数据库程序在C:\PDOXUSRS.NET生成文件,拒绝访问及读写权限, "无法打开 PARADOX.NET.这个文件可以随便删除的,下次会自动产生. Permission ...

KLEE--KLEE主要的生成文件解读

KLEE--KLEE主要的生成文件解读相关推荐

最新文章

热门文章