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] Question about Forward Slicing



2016-09-01 11:18 GMT+02:00 Divya Muthukumaran <divya84 at gmail.com>:
> Hi Virgile,
>
> Thanks. I just tried the impact analysis on the program. This is the
> command-line I used - frama-c -impact-pragma main -impact-slicing test.c
> -then-on "impact slicing" -print -val -slevel 20 -calldeps
>

There are two issues. First, be careful that -slevel 20 -calldeps
occurring after the -then-on, they are not taken into account for the
impact analysis (in fact, since the only thing you do on the impact
slicing project is to print the code, these options are useless
there). Second, impact itself is only meant to print (or highlight in
the GUI) the statements that are impacted by the current selection.
-impact-slicing launch a slicing (in the Slicing plug-in sense, i.e.
backwards), whose criterion is to preserve the statements that have
been selected by the impact analysis itself. It makes thus the same
approximations than the Slicing plugin, in particular, as Patrick
said, it does not take into account the information given by the
-calldeps option to distinguish between the two call to cpy.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile