Hi Juan,
The warnings say that no implementation for these functions is
available. You should compile uclibc with support for these functions.
However, note that mainline KLEE does not have support for symbolic
floating point operations, but there are a couple of (open-source but
unmaintained) extensions of KLEE which do:
https://srg.doc.ic.ac.uk/publications/17-klee-n-version-fp-ase.html
Best,
Cristian
On 07/01/2021 10:26, juanfrancisco.garcia wrote:
I'm getting this warnings for all math.h functions,
KLEE: WARNING ONCE: calling external: floor(9221120237041090560)
KLEE: WARNING ONCE: calling external: round(0)
math.h is included, and if I change libc to uclibc I also get this
warnings:
KLEE: WARNING: undefined reference to function: acos
KLEE: WARNING: undefined reference to function: atan2
KLEE: WARNING: undefined reference to function: ceil
KLEE: WARNING: undefined reference to function: cos
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: round
KLEE: WARNING: undefined reference to function: sin
KLEE: WARNING: undefined reference to function: sqrt
Are math.h functions supported in klee?
I also tried with z3 solver that supports floating point, and it gives
the same warnings.
Thanks in advance,
Juan Francisco García
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
