--- layout: fc_discuss_archives title: Message 6 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, 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