问题标签 [klee]

http://klee.llvm.org/是一个程序分析工具，它通过符号执行和约束求解来工作，找到可能导致程序崩溃的输入，并将它们作为测试用例输出。这是一个非常令人印象深刻的工程，迄今为止已经产生了一些良好的结果，包括在 Unix 实用程序的开源实现集合中发现了许多错误，这些实用程序被认为是有史以来编写的一些经过最彻底测试的软件。

我的问题是：它不做什么？

当然，任何此类工具都有其固有的局限性，即它无法读取用户的想法并猜测输出应该是什么。但撇开原则上不可能的事不谈，大多数项目似乎还没有使用 Klee。当前版本的限制是什么，它还不能处理什么样的错误和工作负载？

我正在使用一个名为 KLEE 的测试生成工具，它为我的 C99 代码创建了大量测试。之后我运行测试并使用 gcov 检查线路覆盖率。成功完成后，Gcov 似乎会在运行结束时更新覆盖率数据。

但是，某些测试会失败（断言不正确的语句），这会导致程序中止，并且 gcov 不计算此次运行中涵盖的行数。

有什么方法可以让 gcov 在任何退出时刷新信息（不仅在成功时）？

语境

我正在研究 klee (http://klee.llvm.org) 分支，并希望清理我们的存储库以将我们的东西与“规范”的 klee 代码分开。无论如何，我无法理解/扩展构建系统。

问题

中的目录结构/lib/如下所示

Mine是我刚刚添加的，到目前为止我们把所有东西都扔进去了Core，我正在把它移到Mine. 我如何告诉构建系统正确执行此操作？

我的尝试

由于无法自己解决这个问题，我编辑了/lib/Makefile：

并在更改为时复制/lib/Core/Makefile到。/lib/Mine/MakefileLIBRARYNAME=kleeCoreLIBRARYNAME=kleeMine

警告

我觉得这不是正确的方法，我宁愿修改一些配置脚本或其他东西。它也没有链接（虽然它编译）。

我试图为一个项目设置 Klee，并且在按照http://klee.llvm.org/TestingCoreutils.html测试 coreutils 时遇到了困难

问题很可能是 llvm 构建本身，而不是 Klee，因为当我使用 llvm-dis 分解 .bc 文件时，只有模块 ID 存在，没有实际代码

查看构建输出，让我感到奇怪的是：

任何想法都会被重视。

我正在使用一个程序（klee）来测试 c 代码。我需要在我的程序中使用结果。

它不是可读的信息，但有些解决方案是十六进制数据，格式如下：'\x0e\x00\x00\x00' 我已经询问过如何将其转换为整数，我找到了解决方案。

我也必须在结构中引入这种结果，我会知道大小，但会知道字段或其他任何相关信息。

我想我可以解决这个问题，但现在的问题是，有时您可以获得以下内容： '\n\x00\x00\x00'= 13 或 '\r\x00\x00\x00' = 10

而且我没有找到他们使用哪种表示形式将其转换为可读信息。显然我可以在 python 中解决这个问题： import struct selection = struct.unpack('

我对pyton一无所知，我想在java或c中找到一个解决方案。非常感谢

对于带有符号参数的循环，我有一个关于 KLEE（符号执行工具）如何工作的问题：

如果我们用这段代码执行 klee，它只会给出一个测试用例。但是，如果我们去掉 printf(...) 的注释，klee 将需要某种类型的控制来停止执行，因为它会产生 n 的值：--max-depth= 200

我想了解为什么 klee 有这种不同的行为，这对我来说没有意义。为什么如果我在这段代码中没有 printf，它不会产生相同的值。

我发现它发生在选项时发生 - 当它没有相同的行为时，使用时式。有人知道 Klee 的 --optimize 是如何工作的吗？

另一个同样的问题是，如果在他们发表的论文中，据我所知，他们说他们的启发式搜索将使它不是无限的（他们使用避免饥饿），因为我让它运行不会停止，这是真的在这个循环的情况下应该完成 klee 执行？

提前致谢

我无法重现本文图 7 中的结果：

http://www.stanford.edu/~engler/klee-osdi-2008.pdf

具体来说，我尝试测试核心 util 的“tac”命令：

但是，我没有看到 KLEE 报告的任何错误消息，尽管该论文声称应该存在错误。

另一方面，如果我像这样测试核心 util 的“md5sum”命令：

KLEE 报以下错误：

有人可以指出正确的方向来发现“tac”或“pr”命令中的错误吗？如果这些都需要文件“t2.txt”和“t3.txt”，它们分别在论文中定义为“\b\b\b\b\b\b\b\t”和“\n”。

将不胜感激所有/任何建议。

我是一个尝试使用 KLEE 的初学者。我在使用 pthread 的 C++ 程序上使用 KLEE 自包含包。我生成了一个 .o 文件并使用 KLEE 和以下选项

但我看到我收到警告

在 .bc 文件上使用 klee 也会给我同样的结果。

我不确定为什么我会得到对 pthread 函数的未定义引用。我不确定是否正确使用了 pthreads 库。有没有办法确保这一点？使用 llvm-ld 也无济于事。

下面是我使用的 llvm-ld 命令

我不确定为什么会出现分段错误。当我通常编译程序g++并运行可执行文件时，该程序运行良好。

有人能告诉我哪里出错了吗？

我是 Klee 的新手，所以我开始制作教程。

如果用于编译，我使用：

1. llvm-gcc --emit-llvm -c -g get_sign.c 然后我尝试使用 klee get_sign.o 运行我收到错误：KLEE: ERROR: error loading program 'get_sign.o': Invalid MODULE_CODE_GLOBALVAR record 。该错误在 BitcodeReader.cpp 文件 http://llvm.org/docs/doxygen/html/BitcodeReader_8cpp_source.html 第 01594 行中定义。

2. clang（我已成功用于我的 LLVM 通行证），似乎无法使用它： KLEE: ERROR: error loading program 'get_sign.o': Invalid bitcode signature 。

你知道我能做什么吗？

此外，最好提供使用 Clang 编译的 Klee 输入，这些输入已经用于我的通行证，但正如错误所暗示的那样，这可能吗？

先感谢您 ！

在我的 LLVM 2.9 上安装 Klee 时（根据需要），我遵循了http://klee.llvm.org/GetStarted.html ，意思是：

1. 安装依赖完成

   export C_INCLUDE_PATH=/usr/include/i386-linux-gnu/完毕

   export CPLUS_INCLUDE_PATH/usr/include/i386-linux-gnu/完毕

2. 构建 LLVM 2.9 完成

   安装 llvm-gcc 完成

   将 llvm-gcc 添加到我的 PATH DONE

   导出路径=$PATH:/home/alex/llvm2.9/llvm/llvm-gcc-4.2-2.9-i686-linux/llvm-gcc-4.2-2.9-i686-linux/bin/

   下载并构建 LLVM 2.9 完成

3. --with-cryptominisat2使用at configuration 和make OPTIMIZE=-O2 CFLAGS_M32= installat make ulimit -s unlimitedDONE构建 STP DONE
4. 使用 llvm-gcc DONE 构建 uclibc
5. svn klee 完成

6. 配置 KLEE DONE

   。/配置--with-llvm=/home/alex/llvm2.9/llvm/ --with-stp=/home/alex/llvm2.9/llvm/stp/ --with-uclibc=/home/alex/llvm2.9/llvm/klee-uclibc-0.02-i386/ --with-llvm-build-mode=Release+Asserts --enable-posix-runtime

7. 建造 KLEE 完成

   和ENABLE_OPTIMIZED=1

   没有错误，但我有警告“ /home/alex/llvm2.9/llvm/klee/Makefile.rules:1175: Bytecode libraries require LLVM capable compiler but none is available ****”

但是，当我尝试教程时，出现段错误：klee：错误：找不到链接器输入' /home/alex/llvm2.9/llvm/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'

它们在 Klee 编译期间根本没有构建。你能告诉我我能做什么吗？也许我的问题与这个线程有关： http: //thread.gmane.org/gmane.comp.compilers.llvm.klee/923。

感谢您的任何帮助 ！