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

  • Subject: [Frama-c-discuss] WP-RTE : Invisible nested requires in behavior
  • From: simon.chollet-stg at systerel.fr (simon)
  • Date: Fri, 6 Jul 2018 18:07:47 +0200
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>