--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on April 2009 ---
> In the abstract domain, there's no way to > define the set of all floats which are strictly greater than 0.0, we > can only represent the set of floats which are greater than or equal to > 0.0. Hence, if we already know that x>=0.0, adding /*@ assert x > 0.0; > */ does not give any information that value analysis can use, at least > not until a more precise abstract domain is designed. Virgile is exactly right. The abstract value for a floating-point expression is represented as a closed interval (i.e. of the form [l ; u]). It would be very easy to represent an open-ended interval (when I was studying mathematics, this was written for instance ]0.0; 1e308]). Floating-point values constitute a discrete type, and there exists a value m, around 1e-308, such that x > 0.0 is equivalent to x >= m. Consequently, the interval above could be represented as [m; 1e308]. But did you notice this discussion assumes from the beginning that all floating-point types are doubles? This is because the value analysis assumes that all floating-point types are doubles (hey, it does warn you that "float support is experimental"). So the prerequisite for handling strict inequalities such as x > 0.0 is in fact to build the support for 32-bit floats, otherwise, it would be rather meaningless, and even more incorrect that it is now in the presence of "float" expressions in the analyzed program. Pascal