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: Tue, 7 Apr 2009 16:46:16 +0200
  • In-reply-to: <EF39C507-63AE-466B-A3B2-3E7A0EFE8A1E@cea.fr>
Hello Pascal,
 
Thanks for your answer! (I totally by-passed -simplify-cfg 'cause I too rapidly read and mis-interpreted the help mentionning a "removal" operation <:o)) ... Sorry for that!)
 
Just to complete your response:
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).
 
Cheers,
Dillon
 


________________________________

	De : Pascal Cuoq [mailto:Pascal.Cuoq at cea.fr] 
	Envoy? : mardi 7 avril 2009 16:05
	? : Frama-C public discussion
	Objet : Frama-C : Value Analysis : SWITCH vs IF
	
	
	This example was provided outside the list. 
	 

		typedef struct { float u; float y;} LABS;
		void abs (LABS *p)
		{
		  switch (0.0 < p->u)
		  {
		    case 0 :
		      p->y = -p->u;
		      break;
		    default :
		      p->y = p->u;
		      break;
		  }
		}
		 
		 "frama-c -val -slevel 100 foo.c" 


	The author is concerned that the value analysis fails to
	determine that p->y is a positive float.

	Unfortunately there are a number of limitations to work around:

	1/ Frama-C must be told to turn the switch into cascading if-then-elses
	with the option -simplify-cfg

	2/ The value analysis does not handle strict comparisons between
	floats (such as 0.0 < p->u) and treats them conservatively as if
	equality was possible.

	3/ To treat this example automatically, the value analysis would have
	to handle the relationship between the fact that the condition is 0 or 1
	and the value in p->u. Unfortunately, this is one more indirection than
	it can handle.

	You can separate the cases beforehand so that it notices the
	relationship, but then you have to be careful about point 2/ above
	(any substate where the condition 0.0 < p->u can be both true or
	false is necessarily approximated, and because of 2/ you have to
	have such a substate, so you need to make this
	substate as small as possible).

	The example, revisited :

	typedef struct { float u; float y;} LABS;
	void abs (LABS *p)
	{
	  //@ assert p->u >= 0.0001 || 0. <= p->u <= 0.0001 || p-> u <= 0.;
	  switch (0.0 < p->u)
	  {
	    case 0 :
	      p->y = -p->u;
	      Frama_C_show_each_A(p->y);
	      break;
	    default :
	      p->y = p->u;
	      Frama_C_show_each_B(p->y);
	      break;
	  }
	}

	Command line :

	frama-c -val -slevel 100 /tmp/t.c  -main abs -simplify-cfg -context-width 1 -context-valid-pointers

	Results:

	/tmp/t.c:4: Warning: Assertion got status valid.
	-> the assertion is used as a hint but does not entail any
	additional proof obligation.

	Values for function abs:
	  star_p[0].u ? [-1.79769313486e+308 .. 1.79769313486e+308]
	        [0].y ? [-0.0001 .. 1.79769313486e+308]
	-> almost what you wanted :(

	Sorry for the disappointing results in this case.

	Pascal


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090407/61f12801/attachment.htm