--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on April 2009 ---
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. The only way I see to overcome the current situation is to validate the assert by means of Proof of Programs (Jessie), and to replace it with the appropriate non-deterministic statement ... something like " p->y = Frama_C_float_interval ( 0.0, my_max_float ) ". Is it right? Hence, from a final user point of view, it will be much more cumfortable to get a warning from the Value Analysis when an assert is "Unknown" (the user is responsible of considering warnings as spurious or founded ones), but to make the analysis take into account the assert as "Valid" for the rest of the control flow, if it can be "propagated" so. If this is not implemented, I guess it is far from being so "easy" or even feasible!! Thanks for your opinion and remarks! Dillon -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090408/b356ff78/attachment.htm