[klee-dev] Simple code for KLEE

[Aleksandr Malyutin]

Hi,

I tried to use klee on simple c-code example:

#include <stdio.h>

int plus(int first){
                  if(first+2 == 4)return 1;
                  return 0;
}

int main(int argc, char *argv[]){
                   if(argc == 2) return plus(atoi(*argv[1]));
                   return -1;
}

My steps were:

1)      Create object file by:

llvm-gcc --emit-llvm -c 2plus2.c



2)      Generate test-cases:

klee --posix-runtime 2plus2.o --sym-arg 1

KLEE: NOTE: Using model: /home/malyutin/klee/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/malyutin/klee/klee/examples/my_example/klee-out-0"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: __fgetc_unlocked
KLEE: WARNING: undefined reference to function: __fputc_unlocked
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to function: atoi
KLEE: WARNING: undefined reference to function: endutent
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: getutent
KLEE: WARNING: undefined reference to function: realpath
KLEE: WARNING: undefined reference to function: setutent
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: undefined reference to function: utmpname
KLEE: WARNING ONCE: calling external: __xstat64(1, 53487840, 53587488)
KLEE: WARNING ONCE: calling external: atoi(53548944)

KLEE: done: total instructions = 581
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1


3)      After that I checked resulting test-case:

ktest-tool klee-last/test000001.ktest


ktest file : 'klee-last/test000001.ktest'
args       : ['2plus2.o', '--sym-arg', '1']
num objects: 2
object    0: name: 'arg0'
object    0: size: 2
object    0: data: ' \x00'
object    1: name: 'model_version'
object    1: size: 4
object    1: data: '\x01\x00\x00\x00'

It's simple to see that klee generates test-case for one of three branches. Maybe my code is incorrect or my method for generating test-cases is wrong, but all my attempts to get three test-cases for three branches of my program were absolutely useless.

Help me please and say what I do wrong.

Many thanks,
Aleksander.


-------------- next part --------------
HTML attachment scrubbed and removed