[klee-dev] math.h functions interpreted as external

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev