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



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