--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on March 2020 ---
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>