问题标签 [klee]

我正在使用 KLEE 生成功能测试数据。但是KLEE生成的测试数据让我有些烦恼。

输入：

这是KLEE中的测试数据：

在这个测试用例中，我了解到变量 a 的大小是 40 字节。意思是每块有四个连续数（例如，第一个块\xa0\xff\xff\xff代表一个整数）。然而，什么是货币价值\xa0\xff\xff\xff？

当我在安装 Klee之前尝试安装 LLVM 3.4 时出现此错误。

源代码从 LLVM 官方网站下载，并从 Klee 解压缩到单独的文件。llvm-3.4 目录中的 Makefile 用于构建 LLVM。

要构建 Klee，首先：

和错误：

似乎这个错误是从 Klee 抛出的，但正如 Klee 指南所说，我的 LLVM 版本没有问题。

此处和此处发布了另一个类似的问题，但没有帮助。

我仍然不知道从哪里开始调试。我感谢任何可能的帮助。

我想在使用 ghc 前端和 llvm 后端编译 haskell 文件生成的 .bc 文件上运行 klee。

我的 haskell hello.hs 文件中有以下代码：

我使用以下命令用 ghc 编译 hello.hs

它会生成一个 hello.ll 文件以及其他文件。然后我尝试将此 .ll 文件编译成 .bc 文件。

问题是当我尝试运行 klee 或尝试在 .bc 文件上运行 lli 时出现以下错误

我在 docker 上运行 ghc 和 llvm。我有 llvm 3.4 版和 ghc 7.6.3 版。

我正在尝试在 Ubuntu 16.04 LTS 中安装 klee ( http://klee.github.io/build-llvm34/ )。我有clang-3.9。在 klee_build_dir 中执行以下命令后，我有带有 klee-stats 和 ktest-tool 的 bin 目录，但没有 klee。请帮忙

我有一个 KLEE 的修改版本和一个基本上简单的查询，例如

当我调用 Z3 求解器时，我在 z3/src/ast/rewriter/rewriter_def.h 中的以下 while 语句中陷入了无限循环（虽然没有永远等待:]）：

我已经在GitHub/Z3Prover/z3/issues 中将它作为一个潜在的错误发布， 但我完全不确定这确实是一个错误。非常感谢任何帮助，谢谢！

我将 Klee 安装为 docker 映像。我正在尝试遵循 KLEE 的第一个教程。我想知道不是通过 echo "int main(int argn, char** argv) { return 0; }" > test.c 输入源代码，如何将 .c 文件输入到 home/klee？

谢谢。

我想避免进行程序间符号执行。也许有一个没有任何约束的返回值，并且可能解析为任何可能的具体值。

这样的事情甚至可能吗？

我想这样做的原因是我想避免执行某些具有非常大循环并且不真正修改全局数据的函数。

每个生成的测试都相当于一条路径，我有兴趣获取有关沿每条路径调用的函数的信息，并从那里获得一个调用图作为所有测试的路径的联合。

考虑到符号变量、假设等，这​​应该呈现完整调用图的子集。

有没有人调查过这个？（也许这已经成为可能，无需更改 KLEE 源代码。）

最好的问候每林格伦

我正在我的码头集装箱中探索 KLEE 附带的玩具“get_sign.c”程序。我想探索执行符号计算的不同路径：

我可以看到符号计算器通过以下方式插入的值：

但是现在我也想看看实际的路径，如果有这样的选项，或者至少我想看看每条路径对应的路径条件。最后，我希望能够看到最长/最短路径是什么，并探索它们的路径条件。

我正在搜索 klee-last 目录并查看这些文件，但我没有在这些 .txt 文件和消息中看到有关路径条件的任何明确信息，除非我是并且我不认识它们。

我是使用 Linux 和 cmake 的新手。想在ubuntu14.04搭建KLEE系统时遇到了一些麻烦。当我来到官方页面所说的第8部分时。见本页： http: //klee.github.io/build-llvm34/

它使用 -std=14 的 c++ 标准有问题，但我不知道为什么我的编译器不支持它。

所以我的问题是：1.是否有必要使用C++ 14？2.如果不是，我该如何更改编译器使用的版本以避免这种错误？

llvm 是 3.4 clang 是 3.4