Error message No applicable tactic for line semax_func_cons body_sumarray.

[eleehiga]

Currently I am using coqide to step through the proof from here: https://github.com/PrincetonUniversity/VST/blob/master/progs/verif_sumarray.v. However in this block of code:

(*#[export] *)
Existing Instance NullExtension.Espec.

Lemma prog_correct:
  semax_prog prog tt Vprog Gprog.
Proof.
  prove_semax_prog.
  semax_func_cons body_sumarray.
  semax_func_cons body_main.
Qed.

At the line semax_func_cons body_sumarray. that yields the error message No applicable tactic. Was wondering if you guys could please assist me with how to solve this error?

[mansky1]

I looked into this, and I think it's a bitsize issue. By default VST is set up for 64-bit programs, but the progs examples are 32-bit. This mostly doesn't change the proofs (as you can tell from the fact that you got that far), but something seems to get stuck at the very end. If you try the same thing in the progs64 folder, it should work completely.

[eleehiga]

@mansky1 Thank you the progs64 version worked completely. Perhaps you guys should note somewhere that people should run the tutorials from the progs64 folder.