遇到forward_call问题 - "no applicable tactic"

Question

我正在读软件基础第5册。

使用body_push_increase (verify -triang)时，我正试着把推电话转过去。前面的上下文是:

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

我正在尝试的命令是

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

出错，提示

Error: No applicable tactic.

push的规格为

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)

(C说typedef struct cons *stack;而不是只有一个元素的堆栈结构)

我做错了什么?

Answer 1

…结果我忘了输入&;gvars &; gv&;在早期的forward_while中。这不是一个明显的陷阱。

Answer 2

确实，"错误:无适用策略";不是一个很有用的信息。在VST 2.7和VST 2.8之间，对"forward"命令打印的错误诊断进行了一些改进;和";forward_call"策略。当我有机会时，我将检查这种情况现在是否在VST 2.8中给出更好的消息。