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?

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>