KLEE WARNINGS и никакие входные данные не сгенерированы

Я новичок в 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, это также должно позволить обрабатывать функции.

Может ли кто-нибудь помочь мне с этим?


И если я не использую --libc=klee во время выполнения 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

Та же ошибка, другие предупреждения.


person Urmas Repinski    schedule 03.03.2013    source источник
comment
Покажите нам код tcas.c.   -  person arrowd    schedule 05.03.2013


Ответы (1)


Кажется, что KLEE-версии uclibc недостаточно. Если вы запустите кли с klee --libc=uclibc, вы не получите этого предупреждения.

person afsafzal    schedule 30.06.2016