c - KLEE WARNINGS 并且没有生成任何输入

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);
} 

我得到了预期的结果:

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#build

使用 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

看来 uclibc 的 KLEE 版本不够用。如果您使用 klee --libc=uclibc 运行 klee，您将不会收到该警告。