--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on December 2008 ---
Hi everyone! In this simple program: /*@ requires \valid(a+(0..len-1)) && @ len >= 0 && len < 2147483647 && @ 0<=(len>>3L)<=len; @*/ void f(int *a,int len){ int i = (int)(len>>3L); if(i>0) { while(1){ a+=8; if(--i==0) break; } } } I?m trying to discharge all the safety conditions that are automatically generated (with Frama-C and Jessie-plugin). There is one particular safety condition that is not proved: integer_of_int32(__jc_off_a0) + 8 <= 2147483647 After doing some code analysis(from the one that is generated from Jessie to Why), I realized that this safety condition is related with the offset of pointer ?a?. So, what I understand is that this safety condition is trying to validate all memory accesses to pointer a. One particular case that can happen during the execution of this code, i.e.: - If len==8, then the valid positions in ?a? are between 0 to 7, and i ==1. - Then, when this computation is executed a+=8, this will point to a invalid memory zone. - But in this particular case, this is irrelevant because I will never use pointer a again - Although this happens, the condition is generated, but it will never be proved. Am I correct? My question is, besides the pre-condition that was added to the code, what are the conditions that I must ensure to prove this particular safety condition? Thanks, B?rbara -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081211/36d26704/attachment-0001.htm