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]

Так что кажется разумным устранить f_get с моей проверенной леммой body_get, Почему тактика терпит неудачу?

Сообщение не помогает:

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

Answer 1

Проблема в спецификации списка аргументов.

• Он должен содержать только аргументы функции (без локальных)

• Он должен иметь аргументы в том же порядке, что и в прототипе функции C.

Кстати, порядок функций в Gprog должен быть таким же, как порядок определений функций в c-файле.