--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on February 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] frama-c "dynamic" slicing?



Hello,

Le mer. 5 févr. 2020 à 18:40, Ivan Postolski <ivan.postolski at gmail.com> a
écrit :

>
> Now I'm having another curious behaviour with the same slicing mode, if I
> have a code like the following:
>
> foo(int x) {
>      if (x > 5) {
>           y = x ;
>      } else {
>           y = 2*x;
>      }
>     return y; //<- slicing criteria
> }
>
> then executing one branch of foo, the if-else condition is not kept in the
> frama-c slice
>
> for instance
>
> main() {
>      foo(6);
> }
>
> will only keep the y=x, return y;
>
> or
>
> main() {
>      foo(3);
> }
>
> will keep the y=2*x return y;
>
> and discard the conditional statements from the slice
>
>
I'm afraid this is unavoidable: the analysis is **too** precise, and the
slicing detects that in this context the test is always true (or false), so
that it does not really have an effect on the value of y at return point. A
quite ugly workaround would be to slightly modify the test so that it has a
side-effect, and ask for the slicing to keep it as well:

int y;

int foo(int x) {
     int if1;
     /*@ slice pragma stmt; */
     if (if1 = x > 5) {
          y = x ;
     } else {
          y = 2*x;
     }
    /*@ slice pragma stmt; */
    return y; //<- slicing criteria
}


int main() {
     foo(6);
}

gets you (frama-c -eva-precision 11 -slice-pragma foo file.c -then-last
-print)

/* Generated by Frama-C */
int y;
int foo_slice_1(int x)
{
  int if1;
  /*@ slice pragma stmt; */
  {
    if1 = x > 5;
    if (if1) y = x;
  }
  /*@ slice pragma stmt; */
  return y;
}

void main(void)
{
  foo_slice_1(6);
  return;
}

If you know OCaml, writing a script to convince Frama-C to add a local
variable, the pragma and the assignment for each if in the program should
be doable.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200205/a9204d84/attachment.html>