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] Safety Conditions in Frama-C

  • Subject: [Frama-c-discuss] Safety Conditions in Frama-C
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Thu, 11 Dec 2008 16:18:45 -0000
  • In-reply-to: <4941048B.5090505@inria.fr>
  • References: <004701c95b7c$fb955530$f2bfff90$@com> <4941048B.5090505@inria.fr>
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