semax_func_cons - 没有适用的策略

Question

我正在尝试将我的两个函数的证明合并为整个程序的证明：

...
Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := get_spec :: set_spec :: nil.

Lemma body_get: semax_body Vprog Gprog f_get get_spec.
Proof.
...
Qed.

Lemma body_set: semax_body Vprog Gprog f_set set_spec.
Proof.
...
Qed.

Existing Instance NullExtension.Espec.


Theorem all_funcs_correct:
  semax_func Vprog Gprog (prog_funct prog) Gprog.
Proof.
semax_func_skipn.
semax_func_cons body_get.

在应用semax_func_cons策略之前，我有以下目标：

1 subgoals, subgoal 1 (ID 3951)

  ============================
   semax_func Vprog [get_spec; set_spec]
     [(_get, Internal f_get); (_set, Internal f_set)]
     [(_get,
      WITH x : share * Z * (Z -> val) * val * val PRE  [
      (_key, tint), (_rez, tint), (_arr, tptr tint)]
      (let (p, varr) := x in
       let (p0, vk) := p in
       let (p1, arr) := p0 in
       let (sh, k) := p1 in
       PROP  (0 <= k < 100; forall i : Z, 0 <= i < 100 -> is_int (arr i);
       repr k vk)
       LOCAL  (`(eq vk) (eval_id _key); `(eq varr) (eval_id _arr);
       `isptr (eval_id _arr))
       SEP  (`(array_at tint sh arr 0 100) (eval_id _arr))) POST  [tint]
      (let (p, varr) := x in
       let (p0, _) := p in
       let (p1, arr) := p0 in
       let (sh, k) := p1 in
       `(array_at tint sh arr 0 100 varr) && local (`(eq (arr k)) retval)));
     set_spec]

所以用我证明的引理 body_get 来消除 f_get 似乎是合理的。为什么战术失败了？

留言没有帮助：

Toplevel input, characters 0-24:
Error: No applicable tactic.

Answer 1

问题出在参数列表规范中。

它必须只包含函数参数（没有本地参数）
参数的顺序必须与 C 函数原型中的顺序相同。

顺便说一句，Gprog 中函数的顺序必须与 c 文件中函数定义的顺序相同。

semax_func_cons - 没有适用的策略

semax_func_cons - no applicable tactic

verifiable-c