时间戳

首页 > 解决方案 > forward_call 遇到问题 - “没有适用的策略”

verifiable-c - forward_call 遇到问题 - “没有适用的策略”

问题描述

我正在阅读软件基础第 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;堆栈没有单元素结构）

我究竟做错了什么？

标签： verifiable-c

解决方案

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

推荐阅读