Turn off implicit promotion of float and double
I have a function f
whose post-condition I want to verify. Following is the function f
along with its ensures clause:
/*@
ensures \result == x - (x*x*x)/6.0f;
*/
float f(float x)
{
return x - (x*x*x)/6.0f;
}
Frama-C, (with WP only) returns "Unknown" as the status of this post-condition. Does this have anything to do with the implicit promotion of floats to reals?
From the ACSL Implementation document (https://frama-c.com/download/frama-c-acsl-implementation.pdf, Section 2.2.5):
Unlike the promotion of C integer types to mathematical integers, there are special float values that do not naturally map to a real number, namely the IEEE-754 special values for “not-a-number”, +∞ and −∞. See below for a detailed discussion on such special values. However, remember that ACSL’s logic has only total functions. Thus, there are implicit promotion functions
real_of_float
andreal_of_double
whose results on the 3 values above is left unspecified.
Is there a way to turn off this implicit promotion of float
to real
?
More importantly, is there a way to verify the post-condition of functions like f
(given above), that involve floating point values?