--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on July 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180710/35b290d0/attachment.html>