--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on October 2019 ---
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>