--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP - Verifiable annotations with some types but not others



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