问题标签 [klee]

我最近在玩 KLEE。我按照文档“ Building KLEE (LLVM 3.4) ”成功运行了教程中的所有示例。

但是，当使用 KLEE 运行我自己的程序时：

发生了一些错误。（请参阅以下控制台输出）

我很好奇为什么会出现与 uclibc 相关的错误？因为我按照 KLEE 文档所说的那样编译它，并且在编译之前“配置” uclibc 时，我没有找到任何禁用汇编代码（例如 no-asm）的选项。

此外，我还注意到有很多关于“undefined reference to function: ...”的警告。我应该将相应的库编译为 llvm 位码而不是使用现有的共享对象吗？

谢谢！

根据他们的论文 (OSDI'08)，符号执行工具 KLEE 需要大约 1 小时来为单个 COREUTIL 应用程序生成测试用例。我想知道它是否可以并行运行？（例如，多核甚至 GPU 上的多线程）？

我想知道当 KLEE 执行涉及变量的指令时，是否有办法判断变量是否在 KLEE 中是符号的。

如何在 KLEE 中将非符号变量（即变量未在输入程序中声明为符号）转换为符号

是否有任何用于在二进制文件上进行符号执行的工具。我的意思是使用哪个，我们不需要修改源代码 - 比如 klee_make_symbolic 或者我们可以在 IR（llvm ir 等）中进行此类更改，提前谢谢

我对 KLEE 很陌生，并尝试安装和测试它。我是按照手工一步步操作的，貌似没有异常错误，但是这个问题是怎么发生的呢？

这是我输入的命令：

我在网上搜索了答案，但不明白这个解释：

“将 llvm-gcc 添加到您的 PATH。首先执行此操作很重要，以便在后续配置步骤中找到 llvm-gcc。稍后将使用 llvm-gcc 来编译 KLEE 可以执行的程序。忘记将 llvm-gcc 添加到到目前为止，您的 PATH 是新用户报告的最常见的构建错误来源。”

有人像我一样遇到这种情况吗？

我已经阅读了Klee 教程中的 klee 教程。这非常简单直接。但是，当我在KLEE generated files中检查测试生成的文件时，我没有找到任何文件告诉我测试是通过还是失败？可以有两种方法来验证测试结果。

1. KLEE 足够聪明，知道 3 个测试用例的预期返回值是多少

2. KLEE 只是将返回值转储到文件中的某个位置，开发人员需要自己检查它们。

是这样吗？

如果在一次执行中发现断言失败，KLEE 将报告它，然后忽略它并继续搜索其他执行。那么问题来了：当发现断言失败时，是否有任何配置或技巧可以强制 KLEE 停止搜索？还是我必须对源代码进行修改并重新构建 KLEE 来实现它？希望有启发性的解决方案。提前致谢！

据我了解，我不能klee在 中的程序上使用C++14，因为 llvm-3.4不支持它。

但是，我想知道是否有任何方法、技巧、实验版本等可以让我在 c++14 程序上使用 klee。

我现在正在学习 KLEE，我写了一个简单的代码：

首先，我生成 LLVM 位码，然后对位码执行 KLEE。以下是所有输出：

我想 KLEE 应该给我一个错误，即 q 指针未初始化，但事实并非如此。为什么 KLEE 没有给我一个错误或警告？KLEE不能检测到这个错误吗？提前致谢！