--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on January 2011 ---
Hi Armand, I noticed that I made a mistake while typing the example. But my problem is that WP is on the Carbon version of Frama-C but it's still a beta version. Can I use the beta version without fear ? Or is there a possibility to do it with the Boron version ? Arnaud On Jan 24, 2011, at 10:22 AM, PUCCETTI Armand wrote: > 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss