这段代码有什么问题？
今天，一个 IRC 用户向我发送了这个有趣的 KLEE 示例，我认为它很可爱，所以我应该发布它。如果您不熟悉它，KLEE 是一个用于对 LLVM 代码进行符号执行的工具。它太复杂了，这里无法解释，但就这个例子而言，您只需要知道它试图探索程序中的所有可能路径。
在这种情况下，用户实际上是在跟我说话，因为他认为 KLEE 中存在错误，因为它只找到了一条代码路径。以下是示例
$ cat t.c这里的意思是klee_int("x")创建一个新的符号变量，它可以是任何东西（好吧，任何可能的int).
#include "klee/klee.h"
int f0(int x) {
if (x * x == 1000)
return 1;
else
return 0;
}
int main() {
return f0(klee_int("x"));
}
用户期望程序中有两条可能的路径，一条返回 1，另一条返回 0。但 KLEE 只找到了一条
$ clang -I ~/public/klee/include -flto -c t.c
$ ~/public/klee.obj.64/Debug/bin/klee t.o
KLEE: output directory = "klee-out-5"
KLEE: done: total instructions = 24
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
当我看到这个例子时，我也困惑了一会儿。然而，由于我恰好信任 KLEE，我知道要寻找测试用例中的问题！当然，1000 的平方根不是整数，所以这段代码不可能返回 1。如果我们将 1000 更改为 100，KLEE 会找到两条我们期望的路径
$ cat t.c
#include "klee/klee.h"
int f0(int x) {
if (x * x == 100)
return 1;
else
return 0;
}
int main() {
return f0(klee_int("x"));
}
$ clang -I ~/public/klee/include -flto -c t.c
$ ~/public/klee.obj.64/Debug/bin/klee t.o
KLEE: output directory = "klee-out-6"
KLEE: done: total instructions = 31
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2