Blog

Tag Archives: FLT_EVAL_METHOD

More on the precise analysis of C programs for FLT_EVAL_METHOD==2
Pascal Cuoq on 15 July 2013

Introduction It started innocently enough. My colleagues were talking of supporting target compilers with excess floating-point precision. We saw that if analyzing programs destined to be compiled with strict IEEE 754 compilers was a lovely Spring day at the beach analyzing for compilers that allow excess precision was Normandy in...

Read More

On the precise analysis of C programs for FLT_EVAL_METHOD==2
Pascal Cuoq on 6 July 2013

There has been talk recently amongst my colleagues of Frama-C-wide support for compilation platforms that define FLT_EVAL_METHOD as 2. Remember that this compiler-set value, introduced in C99, means that all floating-point computations in the C program are made with long double precision, even if the type of the expressions they...

Read More