[klee-dev] Simple code for KLEE

[Urmas Repinski]

Hi, Aleksander.
I had found 2 problems, maybe correcting them will solve the question.
Problem N1 i found:
> My steps were:........... > 2)      Generate test-cases:> klee --posix-runtime 2plus2.o --sym-arg 1 ..............
"--sym-arg 1" means that one symbolic argument will be generated, with size 1 bytes, that were generated, argv[1] should be in the program if i understood right:

> object    0: name: 'arg0'> object    0: size: 2> object    0: data: ' \x00'
http://klee.github.io/klee/TestingCoreutils.html  -sym-arg               - Replace by a symbolic argument with length N
Probably it is necessary to use "--sym-args 1 2 1"Then MIN 1 and MAX 2 arguments of size 1 should be generated, this should cover the "return -1" branch.

Problem N2 i found:
There is"KLEE: WARNING: undefined reference to function: atoi" WARNING.
This possibly means that atoi() function does not function correctly when KLEE is executed, i am not sure about it.
I dont know how to use KLEE in this case, but it is possible to generate integer arguments for the plus() function only, and this can solve this problem:
#include <stdio.h> int plus(int first){                  if(first+2 == 4) return 1;                  return 0;} int main(int argc, char *argv[]){
                 int a;                 klee_make_symbolic(&a, sizeof(a), "a");                  return plus(a);                  // return -1;} Then try it:
1)      Create object file by:llvm-gcc --emit-llvm -c 2plus2.c 2)      Generate test-cases:klee --posix-runtime 2plus2.o

This is not exactly that were needed, but, at least, should generate some reasonable output.
Urmas Repinski.
From: Aleksandr.Malyutin at moex.com
To: klee-dev at imperial.ac.uk
Date: Thu, 10 Jul 2014 11:26:35 +0000
Subject: [klee-dev] Simple code for KLEE









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.
 




_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed