--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on July 2012 ---
Not really, I have not take the time to move to the Nitrogen version. But I will ... Regarding my question I tried also: requires \valid_range(&b.val,0,1); Which does the trick. With this solution, the two requires clauses are the only things that are not verified. Arnaud On Jul 6, 2012, at 11:11 AM, Jens Gerlach wrote: > 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 > > _______________________________________________ > 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