--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on April 2009 ---
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