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