[WP] non-matching of strategies with forall and implication
Steps to reproduce the issue
On the attached examples :
-
running the following command
frama-c-gui forall_pattern.c -wp -wp-rte -wp-prover=tip -wp-prop post
to apply a strategy with Instance does not seem to accept the pattern and to match the precondition using
\forall
.strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec. strategy InstanceForall: \tactic("Wp.instance", \pattern(\forall integer _; _), // fails to select the \forall (invalid pattern) // \when(_), // works in this specific example \goal(P_P(i)), \param("P1", i), \children(FastAltErgo) ); proof InstanceForall: post;
-
running the following command
frama-c-gui implication_pattern.c -wp -wp-rte -wp-prover=tip -wp-prop post
to apply a strategy with Cut does not seem to accept the pattern and to match the precondition using
==>
.strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec. strategy CutImplication: \tactic("Wp.cut", \pattern(A ==> _), // fails to select the implication (invalid pattern) // \incontext(A: _ <= 99), // works in this specifi example \param("case", "CASES"), \param("clause", A), \children(FastAltErgo) ); proof CutImplication: post;
Expected behaviour
We would expect \forall
and ==>
to be matched like other acsl expression.
Actual behaviour
Syntax error is reported (Invalid pattern. Ignoring global annotation).
Contextual information
- Frama-C installation mode: opam pin add frama-c https://git.frama-c.com/pub/frama-c.git#64438ed52f9af0052d6f3970202fc48dbc580dba
- Frama-C version: 28.0+dev (commit 64438ed5)
- Plug-in used: WP with why3 1.6.0 and Alt-Ergo 2.5.2
- OS name: Ubuntu
- OS version: 22.04
FYI: @nkosmatov