昨天我问了关于stackoverflow的问题,但是我没有清楚地描述它,所以我改变了提问的方式,也许使问题变得清楚了。
首先,我修改klee提供的示例get_sign.c,将unistd.h包含在程序中,并调用函数sleep()使线程暂停,如下所示

/*
 * First KLEE tutorial: testing a small function
 */
#include <unistd.h>

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");
  sleep(10);
  return get_sign(a);
}


我使用“ llvm-gcc”编译get_sign.c,然后使用klee get_sign.o执行目标文件,线程不暂停,表示sleep()不起作用。
所以我在执行get_sign.o时添加了一个参数,例如klee --libc=uclibc get_sign.o,不幸的是,线程仍然没有挂起,而且,线程报告了一个错误,

KLEE: ERROR: /home/lab/work/klee-uclibc/libc/signal/sigaction.c:58: failed external call: __syscall_rt_sigaction

KLEE: NOTE: now ignoring this error at this location


我该怎么做才能解决这个问题?谢谢!

最佳答案

好像klee使用的信号会使sleep返回得比预期的更快,如http://www.delorie.com/gnu/docs/glibc/libc_445.html 中所示。该参考资料还提供了解决限制的方法。

10-07 18:51