--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on September 2016 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160901/a6bcdf52/attachment.html>