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



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