Hi. Exactly that i suggested too. :) Urmas. > Date: Thu, 10 Jul 2014 14:47:53 +0100 > From: [email protected] > To: [email protected] > CC: [email protected] > 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 > [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
