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