--- layout: fc_discuss_archives title: Message 5 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



Hi Patrick,

Thank you. I'v tried Impact Analysis suggested by Virgile and added another
question about precision of value + impact analysis.

Thanks,
Divya

On Thu, Sep 1, 2016 at 10:22 AM, BAUDIN Patrick <Patrick.Baudin at cea.fr>
wrote:

> Hi,
>
> The slicing plugin performs only backward slices.
>
> The *slice-rd *option uses *Value* plug-in to find statements performing
> a read access to a given memory location.
> Then the slicer performs a backward slice on the value that are read at
> these statements.
>
> That is the reason why the assignment to val1 is not kept.
>
> The second call to cpy is uncessary but kept because the statement
> performing the read access is into that function.
> The use of the option -calldeps of value doesn't help any more.
>
> -- Patrick.
>
>
> Le 01/09/2016 à 09:57, Divya Muthukumaran a écrit :
>
> Hello,
>
> 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.
>
> /*------ Test Program-------*/
> #include <stdio.h>
>
> void cpy(char * dst, char *src) {
>         int i;
>         for(i=0; i<5; i++){
>                 dst[i] = src[i];
>         }
>         dst[5] = '\0';
> }
>
> int main() {
>         char source1[6] = "Hello", source2[6]="World";
>         char dest1[6], dest2[6];
>         char * ptr1;
>         char * ptr2;
>         char val1;
>         char val2;
>         int i=0;
>         cpy(dest1, source1);
>         cpy(dest2, source2);
>
>         ptr1 = dest1;
>         ptr2 = dest2;
>
>        * val1 = *ptr1;*
>         val2 = *ptr2;
>
>         printf("Val 1 = %c\n", val1);
>         printf("Val 2 = %c\n", val2);
>         return 0;
> }
>
> Command:   *frama-c -slice-rd source1 test.c -val -slevel 20 -then-on
> 'Slicing export' -print*
>
>
> /* ---- Result ---------*/
> /* Generated by Frama-C */
> void cpy_slice_1(char *dst, char *src)
> {
>   int i;
>   i = 0;
>   while (i < 5) {
>     *(dst + i) = *(src + i);
>     i ++;
>   }
>   return;
> }
>
> void main(void)
> {
>   char source1[6];
>   char source2[6];
>   char dest1[6];
>   char dest2[6];
>   source1[0] = (char)'H';
>   source1[1] = (char)'e';
>   source1[2] = (char)'l';
>   source1[3] = (char)'l';
>   source1[4] = (char)'o';
>   source2[0] = (char)'W';
>   source2[1] = (char)'o';
>   source2[2] = (char)'r';
>   source2[3] = (char)'l';
>   source2[4] = (char)'d';
>   cpy_slice_1(dest1,source1);
>   cpy_slice_1(dest2,source2);
>   return;
> }
>
> 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.
>
> Thanks,
> Divya
>
>
> _______________________________________________
> Frama-c-discuss mailing listFrama-c-discuss at lists.gforge.inria.frhttp://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
>
>
> _______________________________________________
> 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/ad00fcbb/attachment.html>