--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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