semax_func_cons - no applicable tactic

Question

I'm trying to put together proofs for my two functions into a proof for a whole program:

...
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.

Before application of semax_func_cons tactic, I have the following goal:

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]

So it seems reasonable to eliminate f_get with my proven lemma body_get. Why the tactic fails?

The message does not help:

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

Answer 1

The problem is in the argument list specification.

• It must contain only function arguments (no locals)

• It must have arguments in the same order as in the C function prototype.

BTW, the order of function in Gprog must be the same as the order of function definitions in the c-file.