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: [email protected] To: [email protected] 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 [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
