--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on July 2012 ---
Do you have a particular reason to use the Carbon release? I usually try to stick to the newer releases (Nitrogen, and hopefully soon Oxygen). Jens Von meinem iPad gesendet Am 06.07.2012 um 11:03 schrieb "Arnaud Dieumegard" <arnaud.dieumegard at enseeiht.fr>: > Hi, thanks for the quick reply. > > I added: > requires \forall unsigned char n,m; 0 <= n < 2 && 0 <= m < 2 ==> \valid(&b.val[n]+m); > > but it does not changes anything on unsigned char or unsigned int. > > Arnaud > > On Jul 6, 2012, at 10:55 AM, Boris Hollas wrote: > >> On Fri, 2012-07-06 at 10:37 +0200, Arnaud Dieumegard wrote: >>> typedef struct{ >>> double val[2][2]; >>> }t_struct; >>> >>> t_struct b; >>> >>> /*@ requires \valid(&b.val); >> >> Here, you only specify that val[0][0] is valid. See the ACSL doc on how >> to specify ranges. >> -- >> Best regards, >> Boris >> >> >> _______________________________________________ >> 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 > > Cordialement, > > Arnaud Dieumegard > PhD Student > IRIT-ENSEEIHT / ACADIE > 2 rue Charles CAMICHEL BP 7122 > 31071 TOULOUSE cedex 07 > arnaud.dieumegard at enseeiht.fr > Tel: 05.34.32.21.64 > > > > > > > _______________________________________________ > 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