3

我是 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

同样的错误，其他警告。

4

1 回答 1

1

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

于 2016-06-30T19:48:27.017 回答