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