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: Pascal.Cuoq at cea.fr (Pascal Cuoq)
  • Date: Tue, 7 Apr 2009 16:04:55 +0200
  • In-reply-to: <A6FD74D4A6DA4247AD801E3943634063034F1345@sctex002.st-cloud.dassault-avion.fr>
  • References: <A6FD74D4A6DA4247AD801E3943634063034F1345@sctex002.st-cloud.dassault-avion.fr>
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