--- layout: fc_discuss_archives title: Message 14 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, 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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180706/98857d4d/attachment.html>