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

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*

And indeed, I can now see the assignment to val, and the printf. But I
still see both cpy(), assignment to val2 and the second printf.
You say that this might be because the alias analysis is imprecise?
Wouldn't this be reflected by the results of the value analysis?
For example, this is the result of Value analysis:


[value] ====== VALUES COMPUTED ======
[value] Values at end of function cpy_slice_1:
  i ∈ {5}
  dest1[0] ∈ {72}
       [1] ∈ {101}
       [2..3] ∈ {108}
       [4] ∈ {111}
       [5] ∈ {0}
  dest2[0] ∈ {87} or UNINITIALIZED
       [1] ∈ {111} or UNINITIALIZED
       [2] ∈ {114} or UNINITIALIZED
       [3] ∈ {108} or UNINITIALIZED
       [4] ∈ {100} or UNINITIALIZED
       [5] ∈ {0} or UNINITIALIZED
[value] Values at end of function main:
  source1[0] ∈ {72}
         [1] ∈ {101}
         [2..3] ∈ {108}
         [4] ∈ {111}
         [5] ∈ {0}
  source2[0] ∈ {87}
         [1] ∈ {111}
         [2] ∈ {114}
         [3] ∈ {108}
         [4] ∈ {100}
         [5] ∈ UNINITIALIZED
  dest1[0] ∈ {72}
       [1] ∈ {101}
       [2..3] ∈ {108}
       [4] ∈ {111}
       [5] ∈ {0}
  dest2[0] ∈ {87}
       [1] ∈ {111}
       [2] ∈ {114}
       [3] ∈ {108}
       [4] ∈ {100}
       [5] ∈ {0}
  ptr1 ∈ {‌{ &dest1[0] }‌}
  ptr2 ∈ {‌{ &dest2[0] }‌}
  val1 ∈ {72}
  val2 ∈ {87}

Here, it is clear that val1 and val2 hold different values and the result
of val1 is clearly dependent on source1[0] and that of val2 is dependent on
source2[0].



On Thu, Sep 1, 2016 at 10:09 AM, Virgile Prevosto <virgile.prevosto at m4x.org>
wrote:

> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://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/20160901/485eb9d0/attachment-0001.html>