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

Definition test_sizeof_spec :=
 DECLARE _test_sizeof
  WITH p: val, sh : share, i: Z
  PRE [ _p OF (tptr tint) ]
          PROP  (readable_share sh; 0 <= i <= Int.max_signed)
          LOCAL (temp _p p) SEP (data_at sh tint (Vint (Int.repr i)) p)
  POST [ tint ]
        PROP () LOCAL(temp ret_temp  (Vint (Int.repr 9)))
           SEP (data_at sh tint (Vint (Int.repr i)) p).

Definition Gprog : funspecs := 
        ltac:(with_library prog [test_sizeof_spec]).

Lemma body_test_sizeof_spec: semax_body Vprog Gprog f_test_sizeof test_sizeof_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_test_sizeof test_sizeof_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _b (Vint (Int.add (Int.repr (Zpos xH)) (Ptrofs.to_int (Ptrofs.repr (@sizeof (@cenv_cs CompSpecs) tint)))))) (@cons localdef (temp _a (Vint (Ptrofs.to_int (Ptrofs.repr (@sizeof (@cenv_cs CompSpecs) tint))))) (@cons localdef (temp _p p) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs sh tint (Vint (Int.repr i)) p) (@nil mpred))))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _a tint) (Etempvar _b tint) tint))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _b (Vint (Int.add (Int.repr (Zpos xH)) (Ptrofs.to_int (Ptrofs.repr (@sizeof (@cenv_cs CompSpecs) tint)))))) (@cons localdef (temp _a (Vint (Ptrofs.to_int (Ptrofs.repr (@sizeof (@cenv_cs CompSpecs) tint))))) (@cons localdef (temp _p p) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs sh tint (Vint (Int.repr i)) p) (@nil mpred))))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _a tint) (Etempvar _b tint) tint))) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _b (Vint (Int.add (Int.repr (Zpos xH)) (Ptrofs.to_int (Ptrofs.repr (@sizeof (@cenv_cs CompSpecs) tint)))))) (@cons localdef (temp _a (Vint (Ptrofs.to_int (Ptrofs.repr (@sizeof (@cenv_cs CompSpecs) tint))))) (@cons localdef (temp _p p) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs sh tint (Vint (Int.repr i)) p) (@nil mpred))))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _a tint) (Etempvar _b tint) tint))) POSTCONDITION *)
forward.
Qed.
