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,

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 list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160901/6e12e2f5/attachment.html>