--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on December 2008 ---
Hi! Thanks for your help Claude. I have another question about this extended simple code( the only difference is inside the loop - I'm adding 1 to a[0] and a[7]) /*@ 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) { /*@ loop invariant 0 < i <=(len>>3L) && @ (i>0==> \valid(a+(0..7))); @ loop variant i; @*/ while(1){ a[0]+= 1; a[7]+= 1; a+=8; if(--i==0) break; } } } Is generated a safety condition(with Frama-C Helium) that I'm not able to prove: offset_max(int_P_alloc_table,shift(a,integer_of_int32(__jc_off_a1))) >=7 I tried Litium version, and is generated a similar proof obligation. My question is, what does it means, and what are the conditions must be in pre-conditions(or in loop invariant) to prove this proof obligation. Best regards, B?rbara -----Original Message----- From: frama-c-discuss-bounces at gforge.inria.fr [mailto:frama-c-discuss-bounces at gforge.inria.fr] On Behalf Of Claude March? Sent: quinta-feira, 11 de Dezembro de 2008 12:16 To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] Safety Conditions in Frama-C 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 | _______________________________________________ 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