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 10:41:09 -0000
 

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 

 

 

 

 

 

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081211/36d26704/attachment-0001.htm