--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on February 2020 ---
Hi Virgile Okay, that makes sense, thanks anyway! On Wed, Feb 5, 2020 at 4:16 PM Virgile Prevosto <virgile.prevosto at m4x.org> wrote: > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200205/4c43010c/attachment-0001.html>