Hi Daniel,
Thank you for your answer.
However, when I run klee with uclibc flag, Klee still dumps error message
like this
klee --libc=uclibc input.o
klee: error: Cannot find linker input '/lib/libc.a'
klee: ModuleUtil.cpp:42: llvm::Module* klee::linkWithLibrary(llvm::Module*,
const std::string&): Assertion `0 && "linking in library failed!"' failed.
0 klee 0x089574f8
Aborted
And when I replaced isnan, isinf functions by my own functions called
ismynan, ismyinf, the program still generates warning:
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different target triples!
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).
Please help me answer these.
Thank you,
Thanh
On Thu, Apr 8, 2010 at 8:06 AM, Daniel Dunbar <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> 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
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100409/43782baf/attachment-0001.html
