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> 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
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
>
