--- layout: fc_discuss_archives title: Message 13 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 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