--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on April 2009 ---
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 -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? enlev?e... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090407/0df191d9/attachment.htm