--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RE : Frama-C : Value Analysis : SWITCH vs IF



> 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