Нов съм в 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
Същата грешка, други предупреждения.
tcas.c
. - person arrowd   schedule 05.03.2013