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: ivan.postolski at gmail.com (Ivan Postolski)
  • Date: Tue, 4 Feb 2020 16:46:20 -0300
  • In-reply-to: <CA+yPOVjbTtfi9OUfTh3oEbFVah1a=H9UUKXzty7Mt+mnGi1=EA@mail.gmail.com>
  • References: <CALVmTftYSk5irra0njBzqWaF8V-UHe08GMBK6cLVs=bhH41sYw@mail.gmail.com> <CALVmTfuf6RyoEyY1uLbYNVWe-LjRivU2SBE901h4tEKWhFheJw@mail.gmail.com> <CA+yPOVjbTtfi9OUfTh3oEbFVah1a=H9UUKXzty7Mt+mnGi1=EA@mail.gmail.com>
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>