--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on July 2012 ---
Sorry about that but I did a mistake on my last message. The correct clause was: requires \forall unsigned char n; 0 <= n < 2 ==> \valid_range(&b.val[n],0,1); or requires \forall unsigned char n; 0 <= n < 2 ==> \valid(&b.val[n]+(0..1)); This still does the trick but I can't prove it. Arnaud On Jul 6, 2012, at 11:18 AM, Arnaud Dieumegard wrote: > 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 > > > > > > > _______________________________________________ > 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