--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Safety Conditions in Frama-C



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