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

[Frama-c-discuss] Problem to prove sum in for loop



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>