3

I am new in KLEE.

I had installed klee, followed the instructions correctly.

if i run program from tutorial:

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);
}

I get result as expected:

KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 51
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3

But if i want to execute my program i get:

 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

And no inputs generated.

It seems that current klee installation does not support C functions, but i installed as it were written in tutorial: http://klee.llvm.org/GetStarted.html#build

with uclibc and the POSIX environment model, that should make able to process functions too.

Can somebody help me with that?

And if i do not use --libc=klee during klee execution i get

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

Same error, other warnings.

Urmas Repinski
  • 109
  • 1
  • 6

1 Answers1

1

It seems that the KLEE version of uclibc is not sufficient. If you run klee with klee --libc=uclibc you won't get that warning.

afsafzal
  • 592
  • 5
  • 15