KLEE ПРЕДУПРЕЖДЕНИЯ и няма генерирани входове

Нов съм в 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, което би трябвало да може да обработва и функции.

Може ли някой да ми помогне с това?


И ако не използвам --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 с klee --libc=uclibc, няма да получите това предупреждение.

person afsafzal    schedule 30.06.2016