--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on February 2020 ---
Hi There 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 Cheers Ivan.- On Thu, Oct 24, 2019 at 9:26 AM Virgile Prevosto <virgile.prevosto at m4x.org> wrote: > Hello Ivan, > > On Thu, Oct 17, 2019 at 1:21 AM Ivan Postolski <ivan.postolski at gmail.com> >> wrote: >> >>> Hello >>> >>> I've read somewhere online that a "dynamic" slicing can be achieved with >>> frama-c by running the eva analysis with the setting "-slevel 999999999". >>> Is this an intended behaviour? are there any previous works that report >>> about the quality/properties of such slices? Can these slices really be >>> thought as dynamic? >>> >>> > The setting -eva-slevel 999999999 is a bit arbitrary. What is meant is > that if you start with a perfectly defined initial state, you don't have > any source of imprecision (i.e. use of external functions which are not > stubbed, access to volatile variables), the program terminates, Eva is set > up to be very precise (hence the very high -eva-slevel number, which > nowadays might possibly be replaced with -eva-precision 11), and maybe a > few additional constraints notably on the use of malloc, then Eva will > follow a single execution path and using the Slicing plug-in on this base > will give you a slice corresponding to this precise execution path. > However, in presence of loops, there will still be some differences with a > real dynamic slice: each statement in the body of the loop will be kept in > the slice if it contributes to the slicing criterion for at least one loop > step. If you want to have a finer level of details there, you'll need to > use syntactic loop unrolling (but don't use 999999999 as argument to > -ulevel). > > 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/20200204/89e646e8/attachment.html>