--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on July 2018 ---
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>