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:
1. #include <stdio.h>
2. #include <float.h>
3. #define NAN 0.0/0.0
4. #define INF 1.0/0.0
5. int temp1, temp2, temp3, temp4;
6. int main(void) {
7. float x ;
8. float y ;
9. float z ;
10. #line 6 "test.c"
11. x = (float )3.14;
12. #line 7 "test.c"
13. y = (float )0.0;
14. temp1 = isnan(x);
15. temp2 = isnan(y);
16. if (temp1 || temp2) {
17. z = NAN;
18. } else {
19. if (y == 0) {
20. if (x == 0) {
21. z = NAN;
22. } else {
23. z = INF;
24. }
25. } else {
26. temp1 = isinf(x);
27. temp2 = isinf(y);
28. if (temp1) {
29. if (temp2) {
30. z = NAN;
31. } else {
32. z = INF;
33. }
34. } else {
35. if (x / y > FLT_MAX) {
36. z = INF;
37. } else {
38. if (x / y < FLT_MIN) {
39. z = 0;
40. } else {
41. z = x / y;
42. }
43. }
44. }
45. }
46. }
47. #line 9 "test.c"
48. return (0);
49. }
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100405/614beb1b/attachment.html
