Hello,
I am playing with the recent KLEE-MultiSolver, due to H. Palikareva and C.
Cadar, trying to generate test inputs for floating point programs. I have
just successfully installed the nice tool, with Z3 as well as a couple of
other solvers enabled. My intention is to use KLEE+Z3, in which Z3 should
support both the floating point theory and the theory of real numbers.
However, my installed KLEE+Z3 fails to generate inputs for floating point
programs. Below is the program under test, borrowed from the official
tutorial of KLEE, this time with a floating point input (rather than an
integer):
*#include klee/klee.hint get_sign(double x) { if (x == 0) return 0;
if (x 0) return -1; else return 1;} int main() { double a;
klee_make_symbolic(a, sizeof(a), a); return get_sign(a);} *
Then I run KLEE + Z3 with the commands:
* $ llvm-gcc --emit-llvm -c -g get_sign.c*
* $ klee --use-metasmt=z3 get_sign.o*
The message I got from Terminal:
Starting MetaSMTSolver(Z3) ...
*KLEE: WARNING ONCE: silently concretizing (reason: floating point)
expression (ReadLSB w64 0 a) to value 0
(/home/parallels/Work/klee/examples/get_sign_fp/get_sign.c:8)*
*KLEE: done: total instructions = 27KLEE: done: completed paths = 1KLEE:
done: generated tests = 1*
Observe that KLEE + Z3 concretizes floating point expression to 0,
although Z3 is used; it finds only 1 single path instead of 3 that is
expected.
Is there a way to tell KLEE *not* to concretieze floating point expression
to 0 so KLEE + Z3 can be useful when handling floating point program?
Thanks,
Zhoulai
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
