> In my case, the klee only generates one path and one test. How many > paths and tests that the test generator should generate for my program? > ( I think it should be 32).
Hi Thanh, since you're not marking anything as symbolic, there is only one path through the program, as in a normal execution. Unfortunately, as Daniel mentioned, KLEE doesn't handle symbolic floating point, so you won't be able to use KLEE to test all paths in your program. Best, Cristian > > Please help me answer these. > > Thank you, > > Thanh > > On Thu, Apr 8, 2010 at 8:06 AM, Daniel Dunbar <daniel at zuster.org > <mailto:daniel at zuster.org>> wrote: > > Hi Thanh, > > KLEE doesn't support symbolic floating point currently, mostly just > because STP doesn't support it, although it would probably still be an > option because the performance is likely to be very poor. > > What KLEE currently does is concretize the value (pick some feasible > value, and substitute) whenever it would have to do an operation on > symbolic floating point. > > Your example doesn't have any symbolic values, so I'm not sure what > test case you would want KLEE to generate, but the particular reason > it is failing is because it needs access to an isinf implementation. > uClibc has a libm implementation that you can try linking in to your > program, although we don't have any support for doing that > automatically. > > - Daniel > > On Mon, Apr 5, 2010 at 2:41 PM, Thanh Vo <thanhvv at gmail.com > <mailto:thanhvv at gmail.com>> wrote: > > Hi, > > > > I am using Klee to generate tests for floating point programs. > However, even > > with some simple program, Klee can not generate a full test cases > for the > > program. As with following simple code: > > > > #include <stdio.h> > > #include <float.h> > > #define NAN 0.0/0.0 > > #define INF 1.0/0.0 > > int temp1, temp2, temp3, temp4; > > int main(void) { > > float x ; > > float y ; > > float z ; > > #line 6 "test.c" > > x = (float )3.14; > > #line 7 "test.c" > > y = (float )0.0; > > temp1 = isnan(x); > > temp2 = isnan(y); > > if (temp1 || temp2) { > > z = NAN; > > } else { > > if (y == 0) { > > if (x == 0) { > > z = NAN; > > } else { > > z = INF; > > } > > } else { > > temp1 = isinf(x); > > temp2 = isinf(y); > > if (temp1) { > > if (temp2) { > > z = NAN; > > } else { > > z = INF; > > } > > } else { > > if (x / y > FLT_MAX) { > > z = INF; > > } else { > > if (x / y < FLT_MIN) { > > z = 0; > > } else { > > z = x / y; > > } > > } > > } > > } > > } > > #line 9 "test.c" > > return (0); > > } > > > > Klee terminates with a warning message " undefined reference to > function: > > isinf ". Can you explain what happened to the program ? I also > noticed that > > Klee currently does not support floating point operations. Do you > have any > > intention to develop this extend ? > > > > Thank you in advance, > > > > Thanh Vo. > > > > _______________________________________________ > > klee-dev mailing list > > klee-dev at keeda.stanford.edu <mailto:klee-dev at keeda.stanford.edu> > > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > > > > >
