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

  • Subject: [Frama-c-discuss] Frama-C : Value Analysis : SWITCH vs IF
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Wed, 8 Apr 2009 15:28:21 +0200
	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