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



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.

Arnaud

On Jul 6, 2012, at 11:18 AM, Arnaud Dieumegard wrote:

> 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
> 
> 
> 
> 
> 
> 
> _______________________________________________
> 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