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] Frama-c-discuss Digest, Vol 32, Issue 12

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12
  • From: armand.puccetti at cea.fr (PUCCETTI Armand)
  • Date: Mon, 24 Jan 2011 10:22:08 +0100
  • In-reply-to: <mailman.69.1295694092.31928.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.69.1295694092.31928.frama-c-discuss@lists.gforge.inria.fr>
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