KLEE警告而没有生成任何输入

Question

我是克莱新来的。

我安装了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

看来，KLEE版的uclibc是不够的。如果你用klee --libc=uclibc运行klee，你就不会收到警告。