Я новичок в 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