--- layout: fc_discuss_archives title: Message 38 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



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