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