Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Hello Dillon,

Le mer 08 avr 2009 15:28:21 CEST,
"Pariente Dillon" <Dillon.Pariente at dassault-aviation.com> a ?crit :

> 	In that example, if one must ensure that p->y>=0.0 (if one can't
> afford a "-0.0001" in the followinf computations), a cross-validation is
> then recommended using Jessie.
> 	For instance, //@ assert p->y>=0.0; will be proved by provers,
> and will be used by Value Analysis during the remaining computations
> (even if Value Analysis will not validate it).
> 	 
> 
> Indeed, I'm wrong.
> Frama-C Value Analysis will not consider an assert which was evaluated
> as "Unknown" during the analysis, as "Valid" in the statements following
> this assert.

When encountering an assert which it evaluates to "Unknown", the value
analysis plugin attempts to reduce the set of possible states according
to the assertion, by eliminating states which violate the property.
However, it is not always possible to express the reduced set in the
abstract domain used by the plugin, which may thus be forced to keep
some states which are known to be invalid wrt the assertion. 

If I interpret the mail from Pascal correctly (I do not know exactly
which abstract domain is used over floats, but he will correct me if I'm
wrong), this is the case here. 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.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile