Having trouble with forward_call - "no applicable tactic"

Question

I'm working through Software Foundations book 5.

While working through body_push_increasing (verif-triang), I'm trying to pass through the call to push. The context before is:

Espec : OracleKind
p : val
n : Z
gv : globals
Delta_specs := abbreviate : Maps.PTree.t funspec
Delta := abbreviate : tycontext
H : 0 <= n <= Int.max_signed
i : Z
HRE : i < n
H0 : 0 <= i <= N
POSTCONDITION := abbreviate : ret_assert
===========================
semax Delta (PROP () LOCAL (temp _i (Vint (Int.repr (i + 1)));
                            temp _n (Vint (Int.repr n));
                            temp _p p)
              SEP (stack (decreasing i) p; mem_mgr gv))
            (_push([(_p)%expr; (_i)%expr]);) POSTCONDITION

The command I'm trying is

forward_call (p, i + 1, decreasing i, gv)

which is failing with the message

Error: No applicable tactic.

The specification for push is

DECLARE _push
  WITH p : val, i : Z, l : list Z, gv : globals
  PRE [tptr (tptr (Tstruct _cons noattr)), tint]
    PROP (Int.min_signed <= i <= Int.max_signed)
    PARAMS (p; Vint (Int.repr i)) GLOBALS (gv)
    SEP (stack l p; mem_mgr gv)
  POST [tvoid]
    PROP () RETURN () SEP (stack (i :: l) p; mem_mgr gv)

(The C says typedef struct cons *stack; instead of having a one-element struct for stack)

What am I doing wrong?

Answer 1

… And it turns out I forgot to put in "gvars gv" in an earlier forward_while. Not an obvious pitfall.

Answer 2

Indeed, "Error: No applicable tactic" is not a very informative message. Between VST 2.7 and VST 2.8, several improvements were made in the error diagnostics printed by the "forward" and "forward_call" tactic. When I get a chance, I'll check whether this case now gives a better message in VST 2.8.