c - KLEE警告和不产生输入

Question

我是KLEE新来的。

我已经安装了klee，并正确地按照说明操作。

如果我从教程中运行程序:

int get_sign(int x) {
if (x == 0)
   return 0;
if (x < 0)
   return -1;
else 
   return 1;
}
int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
} 

I get result as expected:

KLEE: output directory = "klee-out-0"
KLEE: done: total instructions = 51
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3 

但是如果我想执行我的程序，我得到:

 urmas-PBL21 src # llvm-gcc -emit-llvm -c -g  tcas/versions/v1/tcas.c
 urmas-PBL21 src # klee  --libc=klee tcas.o
 KLEE: output directory = "klee-out-16"
 KLEE: WARNING: undefined reference to function: __errno_location
 KLEE: WARNING: undefined reference to function: fprintf
 KLEE: WARNING: undefined reference to variable: stdout
 KLEE: done: total instructions = 11
 KLEE: done: completed paths = 1
 KLEE: done: generated tests = 1

不生成输入

当前的klee安装似乎不支持C函数，但我按照教程中编写的方式安装:http://klee.llvm.org/GetStarted.html构建

使用uclibc和POSIX环境模型，这应该也能够处理函数。

谁能帮我一下吗?

---

如果我在执行klee时没有使用——libc=klee，我得到

urmas-PBL21 src # klee   tcas.o
KLEE: output directory = "klee-out-19"
KLEE: WARNING: undefined reference to function: atoi
KLEE: WARNING: undefined reference to function: fprintf
KLEE: WARNING: undefined reference to variable: stdout
KLEE: done: total instructions = 11
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

相同错误，另有警告

Answer 1

看来只有KLEE版本的uclibc是不够的。如果你用klee --libc=uclibc运行klee，你不会得到这个警告。