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