--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on January 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12



On 22/01/2011 12:01, frama-c-discuss-request at lists.gforge.inria.fr wrote:
>
> I'm new at using Frama-C and Jessie.
> I have some code and I would like to prove that it is correct but I can't find a way to do it:
>
> typedef struct {
> 	UINT8 a[3];
> 	UINT8 Sum[3];
> 	UINT8 b[3];
> } S;
>
> S vect;
>
> /*@ requires \valid_range(vect.a,0,2)&&  \valid_range(vect.Sum,0,2)&&  \valid_range(vect.b,0,2);
>   @	assigns vect.a[0..2], vect.Sum[0..2], vect.b[0..2];
>   @	ensures \forall UINT8 m; 0<= m<  3 ==>  vect.Sum[m] == vect.a[m] + vect.b[m];
>   @*/
> void f(){
> 	vect.a[0] = 1;
> 	vect.a[1] = 2;
> 	vect.a[2] = 3;
> 	vect.b[0] = 4;
> 	vect.b[1] = 5;
> 	vect.b[2] = 6;
> 	
> 	/*@ loop invariant 0<= i<= 3;
> 	 @	loop invariant \forall UINT8 m; 0<= m<  3 ==>  vect.a[m]==\at(vect.a[m],Here)&&  vect.b[m]==\at(vect.b[m],Here);
> 	 @	loop invariant \forall UINT8 m; i<  m<  3 ==>  vect.Sum[m] == \at(vect.Sum[m],Pre);
> 	 @	loop invariant \forall UINT8 m; 0<= m<  i ==>  vect.Sum[m] == vect.a[m] + vect.b[m];
> 	 @	loop variant 3-i;
> 	 @	loop assigns vect.Sum[0..2];
> 	 @*/
> 	for (UINT8 i=0; i<  3; ++i) {
> 		vect.Sum[i] = vect.Const[i] + vect.Const1[i];
> 	}
> }
>
> I just want to prove that this program does the sum for the vectors.
> The result that I have is:
> 	Impossible to initially prove the second loop invariant
> 	Impossible to prove the preservation of the third loop invariant
>
> Maybe it's due to the side effects of the loop ?
> Do anyone knows if I made a mistake somewhere ?
>
>
Hi,

It would be good if the program compiles. So, you might correct it as 
follows:

typedef unsigned char UINT8;

typedef struct {
     UINT8 a[3];
     UINT8 Sum[3];
     UINT8 b[3];
} S;

S vect;

/*@ requires \valid_range(vect.a,0,2) && \valid_range(vect.Sum,0,2) && 
\valid_range(vect.b,0,2);
  @    assigns vect.a[0..2], vect.Sum[0..2], vect.b[0..2];
  @    ensures \forall UINT8 m; 0 <= m < 3 ==> vect.Sum[m] == vect.a[m] 
+ vect.b[m];
  @*/
void main(){
     vect.a[0] = 1;
     vect.a[1] = 2;
     vect.a[2] = 3;
     vect.b[0] = 4;
     vect.b[1] = 5;
     vect.b[2] = 6;
     int i;

     /*@ loop invariant 0 <= i <= 3;
      @    loop assigns vect.Sum[0..2],i;
      @    loop invariant \forall UINT8 m; 0 <= m < 3 ==> 
vect.a[m]==\at(vect.a[m],Here) && vect.b[m]==\at(vect.b[m],Here);
      @    loop invariant \forall UINT8 m; i <= m < 3 ==> vect.Sum[m] == 
\at(vect.Sum[m],Pre);
      @    loop invariant \forall UINT8 m; 0 <= m < i ==> vect.Sum[m] == 
vect.a[m] + vect.b[m];
      @    loop variant 3-i;
      @*/
     for (i=0; i < 3; ++i) {
         vect.Sum[i] = vect.a[i] + vect.b[i];
     }
}

and then analyse it with -val

$ frama-c-gui -val <your_file>

and try to prove it using the WP plugin.

Armand