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

Hello,

2016-09-01 9:57 GMT+02:00 Divya Muthukumaran <divya84 at gmail.com>:
> I am trying to use the slicing plugin to forward slice the following
> program. My impression from reading the slicing plugin page was that if I
> used the slice-rd option with a variable, then this should result in a
> forward slice (i.e. give you a subset of the program that depends on a read
> of the variable). However, the slice I am getting back seems incorrect.
>
> [snip code]
>
> I'm not sure why the second call to cpy() is included in the slice and also
> why the assignment to val1 is not included. Please let me know if I'v
> misunderstood what slice-rd does.

Indeed, there seems to be a misunderstanding: the slicing plug-in
performs a backward slicing, i.e. starting from a given criterion, it
will select all statements of the original program on which the
criterion depend. In your case, it must preserve cpy(dest1, source1)
and the definition of the content of source1. Of course,
over-approximations performed by Value Analysis mean that other
statements might be preserved as well because Slicing cannot verify
that they do not contribute to the criterion. I'd guess that in your
case, this is because the two calls somehow let Slicing consider that
source1 and source2 might be aliased (note that incrementing the
slicing-level does not help).

If you want to compute a forward slice, you have to use the Impact
plugin, which can only be controlled through //@ impact pragma stmt;
annotations placed before the statements whose impact you want to
assess, or through the GUI. See  http://frama-c.com/impact.html for
more information. In your example, if you add -calldeps option, the
statement selected by Impact when used over e.g. source1[0] =
(char)'H'; are indeed cpy(dest1, source1); val1 = *ptr1;
and printf("Val 1 = %c\n",(int)val1);

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