--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on February 2020 ---
Hello Virgile Thanks! The inline worked perfectly 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 is there any way to keep the conditional statements in the slice? Cheers Ivan.- On Tue, Feb 4, 2020 at 5:36 PM Virgile Prevosto <virgile.prevosto at m4x.org> wrote: > Hello, > > Le 04/02/2020 à 20:46, Ivan Postolski a écrit : > > Sorry for reviving this thread. To summarize what I've been doing is to > > "emulate" a dynamic slicer with frama-c setting the -slevel to a very > high > > number. Now some of the subjects I'm analyzing contain recursion and > frama-c > > is failing with the following error: > > > > [eva] file.c:449: User Error: detected recursive call > > > > How can I maintain the "single execution path" though recursion? as I > know > > that the program terminates after probably a few recursive calls > > > > Frama-C has the option -inline-calls <f1,...,fn> that instructs the kernel > to inline each call to functions f1, ..., fn. If you know that the number > of > recursive calls has a finite bound, you can inline the recursive function > several times, with e.g. > > frama-c <files.c> -inline f -then -inline f -then -inline f ... -then -eva > > Note that you more or less double the recursion depth that you can handle > for each -then -inline f > > 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/f5ff372e/attachment.html>