--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on January 2011 ---
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