--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on September 2016 ---
[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