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,

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

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