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

Definition h_spec :=
 DECLARE _h
  WITH gv: globals
  PRE [  ]
          PROP  ()
          LOCAL (gvars gv)
          SEP   (data_at Ews tint (Vint (Int.repr 7)) (gv _g))
  POST [ tint ]
        PROP () LOCAL(temp ret_temp  (Vint (Int.repr 7)))
           SEP (data_at Ews tint (Vint (Int.repr 7)) (gv _g)).

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

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

Lemma body_h: semax_body Vprog Gprog f_h h_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y (Vint (Int.repr (Zpos (xI (xI xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr (Zpos (xI (xI xH))))) (gv _g)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_f) Ews Z0 (gv _f)) (@cons mpred (@data_at_ CompSpecs Ews (tarray (Tstruct _foo noattr) (Zpos (xI xH))) (gv _e)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_d) Ews Z0 (gv _d)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_c) Ews Z0 (gv _c)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_b) Ews Z0 (gv _b)) (@cons mpred (@data_at_ CompSpecs Ews (Tstruct _foo noattr) (gv _a)) (@cons mpred (@data_at_ CompSpecs Ews (tptr (Tstruct _foo noattr)) (gv _p)) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _y tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* x = g; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y (Vint (Int.repr (Zpos (xI (xI xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr (Zpos (xI (xI xH))))) (gv _g)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_f) Ews Z0 (gv _f)) (@cons mpred (@data_at_ CompSpecs Ews (tarray (Tstruct _foo noattr) (Zpos (xI xH))) (gv _e)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_d) Ews Z0 (gv _d)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_c) Ews Z0 (gv _c)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_b) Ews Z0 (gv _b)) (@cons mpred (@data_at_ CompSpecs Ews (Tstruct _foo noattr) (gv _a)) (@cons mpred (@data_at_ CompSpecs Ews (tptr (Tstruct _foo noattr)) (gv _p)) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _y tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* return x; *)
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.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews tuint (Vint (Int.repr (Zpos (xI (xI xH))))) (gv _g)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_f) Ews Z0 (gv _f)) (@cons mpred (@data_at_ CompSpecs Ews (tarray (Tstruct _foo noattr) (Zpos (xI xH))) (gv _e)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_d) Ews Z0 (gv _d)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_c) Ews Z0 (gv _c)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_b) Ews Z0 (gv _b)) (@cons mpred (@data_at_ CompSpecs Ews (Tstruct _foo noattr) (gv _a)) (@cons mpred (@data_at_ CompSpecs Ews (tptr (Tstruct _foo noattr)) (gv _p)) (@nil mpred)))))))))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _h (Tfunction Tnil tint cc_default)) (@nil expr)) (Sset _y (Etempvar _t'1 tint))) (Sreturn (@Some expr (Etempvar _y tint)))) MORE_COMMANDS) POSTCONDITION *)
rewrite data_at_tuint_tint.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr (Zpos (xI (xI xH))))) (gv _g)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_f) Ews Z0 (gv _f)) (@cons mpred (@data_at_ CompSpecs Ews (tarray (Tstruct _foo noattr) (Zpos (xI xH))) (gv _e)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_d) Ews Z0 (gv _d)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_c) Ews Z0 (gv _c)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_b) Ews Z0 (gv _b)) (@cons mpred (@data_at_ CompSpecs Ews (Tstruct _foo noattr) (gv _a)) (@cons mpred (@data_at_ CompSpecs Ews (tptr (Tstruct _foo noattr)) (gv _p)) (@nil mpred)))))))))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _h (Tfunction Tnil tint cc_default)) (@nil expr)) (Sset _y (Etempvar _t'1 tint))) (Sreturn (@Some expr (Etempvar _y tint)))) MORE_COMMANDS) POSTCONDITION *)
forward_call gv.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y (Vint (Int.repr (Zpos (xI (xI xH)))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews tint (Vint (Int.repr (Zpos (xI (xI xH))))) (gv _g)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_f) Ews Z0 (gv _f)) (@cons mpred (@data_at_ CompSpecs Ews (tarray (Tstruct _foo noattr) (Zpos (xI xH))) (gv _e)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_d) Ews Z0 (gv _d)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_c) Ews Z0 (gv _c)) (@cons mpred (@init_datalist2pred' CompSpecs Delta gv (@gvar_init type v_b) Ews Z0 (gv _b)) (@cons mpred (@data_at_ CompSpecs Ews (Tstruct _foo noattr) (gv _a)) (@cons mpred (@data_at_ CompSpecs Ews (tptr (Tstruct _foo noattr)) (gv _p)) (@nil mpred)))))))))))) (Ssequence (Sreturn (@Some expr (Etempvar _y tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
Qed.


