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: Claude.Marche at inria.fr (Claude Marché)
  • Date: Thu, 11 Dec 2008 13:16:11 +0100
  • In-reply-to: <004701c95b7c$fb955530$f2bfff90$@com>
  • References: <004701c95b7c$fb955530$f2bfff90$@com>

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                    |