Hi Cristian, Thank you again for your answer. I just fixed the input program and make symbolic to the variables. But, the problem remains because STP then Klee does not support floating point numbers. I also noticed that STP does support real arithmetic. So, how can I make Klee treat variables as real numbers instead of floating point numbers ?
Thank you in advance, Thanh. On Mon, Apr 12, 2010 at 12:00 PM, <klee-dev-request at keeda.stanford.edu>wrote: > Send klee-dev mailing list submissions to > klee-dev at keeda.stanford.edu > > To subscribe or unsubscribe via the World Wide Web, visit > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > or, via email, send a message with subject or body 'help' to > klee-dev-request at keeda.stanford.edu > > You can reach the person managing the list at > klee-dev-owner at keeda.stanford.edu > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of klee-dev digest..." > > > Today's Topics: > > 1. Re: Problems with handling floating point functions > (Cristian Cadar) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 12 Apr 2010 10:21:52 +0100 > From: Cristian Cadar <c.cadar at imperial.ac.uk> > Subject: Re: [klee-dev] Problems with handling floating point > functions > To: klee-dev at keeda.stanford.edu > Message-ID: <4BC2E630.6020504 at imperial.ac.uk> > Content-Type: text/plain; charset=ISO-8859-1; format=flowed > > > 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 > > > > > > > > > > > > > ------------------------------ > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > > End of klee-dev Digest, Vol 18, Issue 12 > **************************************** > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100414/135c4e14/attachment.html
