Anomalous behavior of anonymous 'behavior'
Steps to reproduce the issue
See this code:
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
/*@
requires P != 0;
assigns Q;
ensures Q == 1;
*/
void d() {
Q = 1;
}
//@ assigns Q;
void c() {
d();
}
which is an minimal as I could make it.
Note that a calls b, where b has a always-true behavior. c calls d the same way, but without a behavior. The example is extracted from a larger specification with lots of behaviors.
Actual behaviour
In my environment, the above, run with frama-c -wp
produces
fc $ frama-c -wp behavior.c
[kernel] Parsing behavior.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_exit : Timeout (Qed:0.81ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_call_b_requires : Timeout (Qed:0.78ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_normal : Timeout (Qed:0.77ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_c_call_d_requires : Timeout (10s)
[wp] Proved goals: 7 / 11
Qed: 7
Alt-Ergo 2.4.1: 0 (interrupted: 4)
That is c calling d is fine. a calling b is not.
Expected behaviour
I expect a calling be to behave precisely like c calling d.
It appears that even with a prefix consisting of just requires clauses, WP produces an
anonymous behavior that contains something like assigns \everything
. That then causes
the very mysterious assigns errors that you see above.
Fortunately, now that I know the problem there is an easy workaround -- but prior to that it wasted many days of time.
Contextual information
Frama-C 25.0, built from source, with WP MacOS 12.5