--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?



Hi,

When i using the following command to analysis the function in test.c(code
is following):
frama-c-gui -lib-entry -main example test.c -val

the code below the line 5 is dead code. I understand that it is because the
default context-width is 2. So line 5 is out of bound memory access.

But i want to analysis the function by not treat all code to be dead code
and continue the value analysis procedure.

So here is my question:

1. Whether I can perform value analysis by not enable the acsl,rte or wp
annotation?

2. Whether I can perform value analysis by treat all properties to be valid?

3. Whether I can modify the property status programmatically and then
perform the value analysis once again?


/* test.c */
int example(int *A, int size){  //1
  int sum=0;       //2
  sum += A[0];     //3
  sum += A[1];    //4
  sum += A[2];     //5
  int i = 3;        //6:dead code
  while(i < size){    //7:dead code
    sum += A[i];  //8:dead code
    i++;     //9:dead code
  }        //10:dead code
  return sum;    //11
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130909/ce7125ba/attachment.html>