Require Import VST.floyd.proofauto.
Require Import Recdef.
Existing Instance NullExtension.Espec.
Require Import VST.progs.switch.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Definition twice_spec :=
  DECLARE _twice
    WITH n : Z
    PRE [ _n OF tint ]
      PROP  (Int.min_signed <= n+n <= Int.max_signed)
      LOCAL (temp _n (Vint (Int.repr n)))
      SEP ()
    POST [ tint ]
      PROP ()
      LOCAL (temp ret_temp (Vint (Int.repr (n+n))))
      SEP ().


Definition f_spec :=
  DECLARE _f
    WITH x : Z
    PRE [ _x OF tuint ]
      PROP  (0 <= x <= Int.max_unsigned)
      LOCAL (temp _x (Vint (Int.repr x)))
      SEP ()
    POST [ tint ]
      PROP ()
      LOCAL (temp ret_temp (Vint (Int.repr 1)))
      SEP ().


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

Lemma body_twice: semax_body Vprog Gprog f_twice twice_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_f f_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Ssequence (Sswitch (Etempvar _n tint) (LScons (@Some Z Z0) (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) (LScons (@Some Z (Zpos xH)) (Ssequence (Sset _n (Econst_int (Int.repr (Zpos (xO xH))) tint)) Sbreak) (LScons (@Some Z (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))) (Ssequence (Sset _n (Eunop Oneg (Econst_int (Int.repr (Zpos (xO xH))) tint) tint)) Sbreak) (LScons (@Some Z (Zpos (xI xH))) (Sset _n (Ebinop Oadd (Etempvar _n tint) (Econst_int (Int.repr Z0) tint) tint)) (LScons (@None Z) (Ssequence (Sset _n (Ebinop Oadd (Etempvar _n tint) (Etempvar _n tint) tint)) Sbreak) LSnil)))))) (Sreturn (@Some expr (Etempvar _n tint)))) MORE_COMMANDS) POSTCONDITION *)
forward_if (PROP() LOCAL(temp _n (Vint (Int.repr (n+n)))) SEP()).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (Z.add n n)))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Etempvar _n tint))) MORE_COMMANDS) POSTCONDITION *)
repeat forward; entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (Z.add n n)))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Etempvar _n tint))) MORE_COMMANDS) POSTCONDITION *)
repeat forward; entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (Z.add n n)))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Etempvar _n tint))) MORE_COMMANDS) POSTCONDITION *)
repeat forward; entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (Z.add n n)))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Etempvar _n tint))) MORE_COMMANDS) POSTCONDITION *)
repeat forward; entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (Z.add n n)))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Etempvar _n tint))) MORE_COMMANDS) POSTCONDITION *)
repeat forward; entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (Z.add n n)))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Etempvar _n tint))) MORE_COMMANDS) POSTCONDITION *)
repeat forward; entailer!.
Qed.

Lemma body_f: semax_body Vprog Gprog f_f f_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_f f_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x (Vint (Int.repr x))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sswitch (Etempvar _x tuint) (LScons (@Some Z (Zpos xH)) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sbreak) (LScons (@Some Z (Zpos (xO xH))) Sskip (LScons (@Some Z (Zpos (xI xH))) Sskip (LScons (@Some Z (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))))))))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sbreak) (LScons (@None Z) (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) LSnil)))))) MORE_COMMANDS) POSTCONDITION *)
forward_if (@FF (environ->mpred) _).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x (Vint (Int.repr x))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) (switch_ret_assert (overridePost (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) POSTCONDITION)) *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x (Vint (Int.repr x))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) (switch_ret_assert (overridePost (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) POSTCONDITION)) *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x (Vint (Int.repr x))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) (switch_ret_assert (overridePost (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) POSTCONDITION)) *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x (Vint (Int.repr x))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) (switch_ret_assert (overridePost (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) POSTCONDITION)) *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x (Vint (Int.repr x))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) (switch_ret_assert (overridePost (@FF (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric)) POSTCONDITION)) *)
forward.
Qed.


