[klee-dev] Simple code for KLEE

[Urmas Repinski]

Hi.
Exactly that i suggested too. :)
Urmas.

> Date: Thu, 10 Jul 2014 14:47:53 +0100
> From: daniel.liew at imperial.ac.uk
> To: Aleksandr.Malyutin at moex.com
> CC: klee-dev at imperial.ac.uk
> Subject: Re: [klee-dev] Simple code for KLEE
> 
> Your code uses atoi() which isn't part of your 2plus2 program. Notice
> that KLEE warns about this
> 
> KLEE: WARNING: undefined reference to function: atoi
> 
> and later calls this function
> 
> KLEE: WARNING ONCE: calling external: atoi(53548944)
> 
> An external function, is a function that isn't in the bitcode being
> executed (which is your 2plus2.o code linked with which ever libraries
> you asked KLEE to use. In your case you asked only for the POSIX
> runtime).
> 
> When KLEE encounters an external function it makes the arguments to
> that function concrete and then calls the native function ``atoi()``.
> In your case making arguments to atoi() concrete will cause test cases
> to be lost.
> 
> Try linking with klee-uclibc (use -libc=uclibc) which probably
> provides an implementation of atoi(). If it doesn't you can always add
> your own.
> 
> Note atoi() probably has quite a lot of branching behaviour so you may
> generate many more paths that you might expect. In which case you
> might just want to do something much simpler like this...
> 
> ```
> int plus(int first){
> 
>                   if(first+2 == 4)return 1;
> 
>                   return 0;
> }
> 
> 
> int main(int argc, char *argv[]){
> 
>                    int x;
>                    klee_make_symbolic(&x, sizeof(x));
>                    return plus(x);
> }
> ```
> 
> Hope that helps.
> 
> _______________________________________________
> 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