Require Import VST.floyd.proofauto.
Require Import VST.progs.funcptr.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Local Open Scope Z.
Local Open Scope logic.

Definition myspec :=
  WITH i: Z
  PRE [ _i OF tint ]
          PROP (Int.min_signed <= i < Int.max_signed)
          LOCAL (temp _i (Vint (Int.repr i)))
          SEP ()
  POST [ tint ]
         PROP() LOCAL (temp ret_temp (Vint (Int.repr (i+1))))
          SEP().

Definition myfunc_spec := DECLARE _myfunc myspec.

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE  [] main_pre prog nil gv
  POST [ tint ] main_post prog nil gv.

Definition Gprog : funspecs :=   ltac:(with_library prog [
    myfunc_spec; main_spec]).

Lemma body_myfunc: semax_body Vprog Gprog f_myfunc myfunc_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_myfunc myfunc_spec *)
unfold myfunc_spec.
(* Goal: semax_body Vprog Gprog CompSpecs f_myfunc (@pair ident funspec _myfunc myspec) *)
unfold myspec.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos xH))))) (@cons localdef (temp _f (gv _myfunc)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (func_ptr' myspec (gv _myfunc)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _j tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
Qed.

Lemma body_main: semax_body Vprog Gprog f_main main_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function. fold cc_default noattr tint.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Ssequence (Sset _f (Eaddrof (Evar _myfunc (Tfunction (Tcons tint Tnil) tint cc_default)) (tptr (Tfunction (Tcons tint Tnil) tint cc_default)))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Etempvar _f (tptr (Tfunction (Tcons tint Tnil) tint cc_default))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr))) (Sset _j (Etempvar _t'1 tint))) (Sreturn (@Some expr (Etempvar _j tint))))) MORE_COMMANDS) POSTCONDITION *)
make_func_ptr _myfunc.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos xH))))) (@cons localdef (temp _f (gv _myfunc)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (func_ptr' myspec (gv _myfunc)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _j tint))) MORE_COMMANDS) POSTCONDITION *)
forward.

(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _f (gv _myfunc)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (func_ptr' myspec (gv _myfunc)) (@nil mpred))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Etempvar _f (tptr (Tfunction (Tcons tint Tnil) tint cc_default))) (@cons expr (Econst_int (Int.repr (Zpos (xI xH))) tint) (@nil expr))) (Sset _j (Etempvar _t'1 tint))) (Sreturn (@Some expr (Etempvar _j tint)))) MORE_COMMANDS) POSTCONDITION *)
forward_call 3.
(* Goal: and (Z.le Int.min_signed (Zpos (xI xH))) (Z.lt (Zpos (xI xH)) Int.max_signed) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos xH))))) (@cons localdef (temp _f (gv _myfunc)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (func_ptr' myspec (gv _myfunc)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _j tint))) MORE_COMMANDS) POSTCONDITION *)
  computable.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _j (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos xH))))) (@cons localdef (temp _f (gv _myfunc)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (func_ptr' myspec (gv _myfunc)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Etempvar _j tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
Qed.
