--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on February 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] frama-c "dynamic" slicing?



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>