0

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

在通过 body_push_increasing (verif-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.

推送的规范是

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;堆栈没有单元素结构）

我究竟做错了什么？

4

2 回答 2

1

......结果我忘了在前面输入“gvars gv” forward_while。不是一个明显的陷阱。

于 2021-09-12T15:07:51.087 回答
0

事实上，“错误：没有适用的策略”并不是一个非常有用的信息。在 VST 2.7 和 VST 2.8 之间，对“forward”和“forward_call”策略打印的错误诊断进行了一些改进。当我有机会时，我会检查这个案例现在是否在 VST 2.8 中提供了更好的信息。

于 2021-09-13T12:46:17.463 回答