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 "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>