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,

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>