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