# 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] Frama-c-discuss Digest, Vol 32, Issue 12

*Subject*: [Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12*From*: arnaud.dieumegard at enseeiht.fr (Arnaud Dieumegard)*Date*: Mon, 24 Jan 2011 10:33:42 +0100*In-reply-to*: <4D3D44C0.3000106@cea.fr>*References*: <mailman.69.1295694092.31928.frama-c-discuss@lists.gforge.inria.fr> <4D3D44C0.3000106@cea.fr>

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

**Follow-Ups**:**[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12***From:*jens.gerlach at first.fraunhofer.de (Jens Gerlach)

**References**:**[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12***From:*armand.puccetti at cea.fr (PUCCETTI Armand)

- Prev by Date:
**[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12** - Next by Date:
**[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12** - Previous by thread:
**[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12** - Next by thread:
**[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12** - Index(es):