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

[Frama-c-discuss] While/if conditions and slicing



Hello,

Le ven. 13 mars 2020 à 00:04, Gilbert Pajela <gpajela at gradcenter.cuny.edu>
a écrit :

>
>
> $ cat while.c
> int f() {
>   int x = 1;
>   while (x > 0) {
>     x--;
>   }
>   return x;
> }
> $ frama-c while.c -main f -slice-return f -then-on 'Slicing export' -print
> ...
> /* Generated by Frama-C */
> int f(void)
> {
>   int x = 1;
>   while (x > 0) x --;
>   return x;
> }
>
>
I haven't checked in detail, hence the answer below should be taken with a
grain of salt, but I tend to think that this is due to the way loops are
represented internally by Frama-C. Namely, the Loop AST node does not
contain directly the test. Basically, Frama-C sees something like:

int f() {
  int x = 1;
  while(true) {
    if (! (x>0)) { break; } else { }
    x--;
  }
  return x;
}

The pretty printer recognizes this while(true) { if (...) break; ... }
pattern and presents you with a normal while loop, but the slicer sees the
if and the fact that both branches are taken (the else { } in the first
step and the { break; } in the second step of the loop). Thus, it does not
remove the test, and the code stays as is.

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/20200313/3c87f30e/attachment.html>