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

  • Subject: [Frama-c-discuss] Question about Forward Slicing
  • From: divya84 at gmail.com (Divya Muthukumaran)
  • Date: Thu, 1 Sep 2016 08:57:35 +0100
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>