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] Problem to prove sum in for loop

  • Subject: [Frama-c-discuss] Problem to prove sum in for loop
  • From: arnaud.dieumegard at enseeiht.fr (Arnaud Dieumegard)
  • Date: Fri, 21 Jan 2011 16:13:48 +0100
Hi all,

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 ?

Sincerely,
Arnaud
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110121/056cf42a/attachment.htm>