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] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Subject: [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- From: abiao.yang at gmail.com (David Yang)
- Date: Mon, 9 Sep 2013 01:23:29 +0800
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>
- Follow-Ups:
- [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Prev by Date: [Frama-c-discuss] [Jessie] loop invariant
- Next by Date: [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Previous by thread: [Frama-c-discuss] How would one annotate a function in an external header?
- Next by thread: [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Index(es):