Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] frama-c "dynamic" slicing?
- Subject: [Frama-c-discuss] frama-c "dynamic" slicing?
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- Date: Thu, 24 Oct 2019 14:25:31 +0200
- In-reply-to: <CALVmTfuf6RyoEyY1uLbYNVWe-LjRivU2SBE901h4tEKWhFheJw@mail.gmail.com>
- References: <CALVmTftYSk5irra0njBzqWaF8V-UHe08GMBK6cLVs=bhH41sYw@mail.gmail.com> <CALVmTfuf6RyoEyY1uLbYNVWe-LjRivU2SBE901h4tEKWhFheJw@mail.gmail.com>
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 -------------- section suivante -------------- Une piÃ¨ce jointe HTML a Ã©tÃ© nettoyÃ©e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191024/4a9c63c7/attachment.html>
- Prev by Date: [Frama-c-discuss] frama-c "dynamic" slicing?
- Previous by thread: [Frama-c-discuss] frama-c "dynamic" slicing?
- Next by thread: [Frama-c-discuss] ACSL by Example (version 19.1.0 for Frama-C 19.1)