--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on December 2008 ---
Hi, This is just an "unwanted feature" of the last release, already fixed in the next one. Note that this program is equivalent to a += (len>>3)<<3; without any loop... B?rbara Vieira wrote: > > > 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 > > > > > > > > > > > > > > > > > ------------------------------------------------------------------------ > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |