Handle 80bit floats differently in LLVM frontend
Currently, we do not support the x86_fp80 80bit floating point type in our LLVM frontend.
Executing e.g.
scripts/cpa.sh -generateCFA -clang -32 test/programs/benchmarks/floats-cbmc-regression/float-flags-simp1.i
causes a corresponding AssertionError
.
It might be possible to handle these values as union
s:
union {
long double d;
unsigned int i: 80;
}
This might allow to use a bigger floating point type only if necessary, as that is problematic when checking for overflows.
Another possibility might be to check the size of long double
on the machine, as long double
is sometimes implemented as 80-bit extended precision ([1], [2], C11 standard (IEC 60559 floating-point arithmetic (Annex F), Section F.2)).
This would be consistent to the other cases in the method.
GCC also provides the __float80
tpye.