Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP-RTE : Invisible nested requires in behavior

Hello,

Mainly due to lack of time, the WP manual does not contains such 
information that may be found on the bts (https://bts.frama-c.com).
Of course, that offers no guarantee that all reported bugs will be fixed.
But, Frama-C developers, and also Frama-C users as you said, need to be 
aware that a bug exists.
So, feel free to report additional problems and do not hesitate to 
(re)open task on the BTS in case of issues.

About the behavior you have reported, it has already been identified 
recently by a partner having access to a private bts.
That could explain why the issue is not reported on the public BTS.
This lack of completeness is being corrected and would be fixed into the 
next Frama-C release.

As answered in previous questions about Frama-C support, CEA LIST offers 
commercial licenses including access to the proprietary extensions
and basic support (dedicated BTS, discussion area and early releases 
including bug fixes).
That could be a way to get the support adapted to your needs and avoid 
potential future shortcomings.

Patrick.

Le 10/07/2018 à 16:31, simon a écrit :
> Hello,
>
> Thank you for your response. You said that this behavior has been 
> identified; where could I find documentation about the workings and 
> the limitations of the current implementation of WP ? The 
> documentation listed on frama-c's site isn't very helpful, and so I 
> could avoid potential future shortcomings trying to work with it.
>
> Simon
>
> Le 10/07/2018 à 09:24, BAUDIN Patrick a écrit :
>> Hello,
>>
>> The issue has nothing to do the rte properties.
>> In fact, it could be the same for other properties you want to prove:
>> WP plug-in has an identified lack of completeness in the use of assumes
>> (for proofs into the current function and it callers) clauses written 
>> into
>> behaviors. That has be fixed.
>>
>> Patrick.
>>
>> Le 06/07/2018 à 18:07, simon a écrit :
>>> Hello, I've got a question on the workings of wp-rte
>>>
>>> In the ACSL documentation, this function is written as an example :
>>>
>>> /*@ behavior p_changed:
>>>    @     assumes n > 0;
>>>    @     requires  \valid(p);
>>>    @     assigns *p;
>>>    @     ensures *p == n;
>>>    @ behavior q_changed:
>>>    @     assumes n <= 0;
>>>    @     requires  \valid(q);
>>>    @     assigns *q;
>>>    @     ensures *q == n;
>>>    @*/
>>>  void f(int n, int *p, int *q) {
>>>        if (n > 0) *p = n; else *q = n;
>>>  }
>>>
>>> Supposedly, this contract is equivalent to :
>>>
>>> /*@ requires (n > 0 ==> requires  \valid(p)) && (n <= 0 ==> 
>>> requires  \valid(q));
>>>     @behavior p_changed:
>>>     @     assumes n > 0;
>>>     @     assigns *p;
>>>     @     ensures *p == n;
>>> ...
>>>     @*/
>>>
>>> However, when proving this function in the first case with the 
>>> -wp-rte guards, rte can't seem to prove that the access to p nor q 
>>> is valid.
>>>
>>> When I write the function like in the second case, rte passes like a 
>>> charm.
>>>
>>> Am I missing something over here, or does rte really doesn't support 
>>> nested requires ?
>>>
>>> Thanks,
>>> Simon
>>>
>>> <http://www.systerel.fr>
>>>
>>>
>>> _______________________________________________
>>> Frama-c-discuss mailing list
>>> Frama-c-discuss at lists.gforge.inria.fr
>>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>>
>>
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180723/2c222b7c/attachment.html>