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 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>