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