--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on July 2012 ---
Hi Virgile, About the requires clause proving it's quite logical and I did not thought about it while asking. Thanks for the precisions and for your help. Arnaud On Jul 6, 2012, at 1:43 PM, Virgile Prevosto wrote: > Hello, > > 2012/7/6 Arnaud Dieumegard <arnaud.dieumegard at enseeiht.fr>: >> 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. >> > > First, just a remark: \valid_range is deprecated (use \valid and .. as > you did in the latter version of your requires). > More importantly, you shouldn't need this requirement: your argument > is a struct which contains an array, > so b.val is always a valid block of 4 doubles. In fact all annotations > are proved with Nitrogen and alt-ergo. > In addition, you cannot prove a requires clause directly: it leads to > a proof obligation on the callers of the function > (to ensure that they meet the requirements set up by the function). > Since there is no caller of init in your code, there's nothing to be > proved for the requires. > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > > _______________________________________________ > 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