Require Import VST.floyd.proofauto.
Require Import VST.progs.float.

Instance CompSpecs : compspecs.
(* Goal: compspecs *)
Proof. make_compspecs prog. Defined.

Local Open Scope logic.

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

Definition t_struct_foo := Tstruct _foo noattr.

Definition Vprog : varspecs := (_s, t_struct_foo)::nil.

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

Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
name x1 _x1.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
name y1 _y1.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
name y2 _y2.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
name s _s.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
pose (f :=  PROP () LOCAL (gvars gv)
  SEP (data_at Ews t_struct_foo (Vint (Int.repr 5),
          (Vsingle (Float32.of_bits (Int.repr 1079655793)),
           Vfloat (Float.of_bits (Int64.repr 0)))) (gv _s))).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons mpred (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons mpred (@data_at CompSpecs Ews tuint (Vint (Int.repr (Zpos (xI (xO xH))))) (gv _s)) (@nil mpred))))))) (Ssequence (Ssequence (Ssequence (Sset _t'2 (Efield (Evar _s (Tstruct _foo noattr)) _y tfloat)) (Sset _y1 (Ecast (Etempvar _t'2 tfloat) tdouble))) (Ssequence (Sset _x1 (Efield (Evar _s (Tstruct _foo noattr)) _x tint)) (Ssequence (Ssequence (Sset _t'1 (Efield (Evar _s (Tstruct _foo noattr)) _y tfloat)) (Sset _y2 (Ecast (Etempvar _t'1 tfloat) tint))) (Ssequence (Sset _y1 (Efield (Evar _s (Tstruct _foo noattr)) _z tdouble)) (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))))))) MORE_COMMANDS) POSTCONDITION *)
apply semax_pre with f; subst f. (* factored out "f" to work around a bug
   in Coq 8.4pl6 (and earlier versions back at least to 8.4pl3).
  To exhibit the bug, put the r.h.s. of the "pose" as in place of f
  in the "apply...with".  *)
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons mpred (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons mpred (@data_at CompSpecs Ews tuint (Vint (Int.repr (Zpos (xI (xO xH))))) (gv _s)) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) (Ssequence (Ssequence (Ssequence (Sset _t'2 (Efield (Evar _s (Tstruct _foo noattr)) _y tfloat)) (Sset _y1 (Ecast (Etempvar _t'2 tfloat) tdouble))) (Ssequence (Sset _x1 (Efield (Evar _s (Tstruct _foo noattr)) _x tint)) (Ssequence (Ssequence (Sset _t'1 (Efield (Evar _s (Tstruct _foo noattr)) _y tfloat)) (Sset _y2 (Ecast (Etempvar _t'1 tfloat) tint))) (Ssequence (Sset _y1 (Efield (Evar _s (Tstruct _foo noattr)) _z tdouble)) (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))))))) MORE_COMMANDS) POSTCONDITION *)
 { 
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons mpred (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons mpred (@data_at CompSpecs Ews tuint (Vint (Int.repr (Zpos (xI (xO xH))))) (gv _s)) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) *)
unfold data_at.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons mpred (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons mpred (@field_at CompSpecs Ews tuint (@nil gfield) (Vint (Int.repr (Zpos (xI (xO xH))))) (gv _s)) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@field_at CompSpecs Ews t_struct_foo (@nil gfield) (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) *)
 unfold_field_at (field_at _ t_struct_foo _ _ _).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons mpred (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons mpred (@field_at CompSpecs Ews tuint (@nil gfield) (Vint (Int.repr (Zpos (xI (xO xH))))) (gv _s)) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews t_struct_foo (@cons gfield (StructField _x) (@nil gfield)) (Vint (Int.repr (Zpos (xI (xO xH))))) (gv _s)) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews t_struct_foo (@cons gfield (StructField _y) (@nil gfield)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (gv _s)) (@field_at CompSpecs Ews t_struct_foo (@cons gfield (StructField _z) (@nil gfield)) (Vfloat (Float.of_bits (Int64.repr Z0))) (gv _s)))) (@nil mpred))))) *)
entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs tuint (@nil gfield) (gv _s))) (@type_induction.type_func CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) (fun (t : type) (v : @reptype CompSpecs t) (p : val) => if type_is_volatile t then memory_block Ews (@sizeof (@cenv_cs CompSpecs) t) p else mapsto Ews t p (@repinject CompSpecs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall (_ : @reptype CompSpecs t) (_ : val), mpred) (v : @reptype CompSpecs (Tarray t n a)) => @array_pred (@reptype CompSpecs t) (@Inhabitant_reptype CompSpecs t) Z0 (Z.max Z0 n) (fun (i : Z) (v0 : @reptype CompSpecs t) (v1 : val) => P v0 (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) t) i) v1)) (@unfold_reptype CompSpecs (Tarray t n a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tstruct id a)) => @aggregate_pred.auxiliary_pred.struct_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tunion id a)) => @aggregate_pred.auxiliary_pred.union_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tunion id a) v)) (@nested_field_type CompSpecs tuint (@nil gfield)) (Vint (Int.repr (Zpos (xI (xO xH))))) (offset_val (@nested_field_offset CompSpecs tuint (@nil gfield)) (gv _s))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _x) (@nil gfield)) (gv _s))) (@type_induction.type_func CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) (fun (t : type) (v : @reptype CompSpecs t) (p : val) => if type_is_volatile t then memory_block Ews (@sizeof (@cenv_cs CompSpecs) t) p else mapsto Ews t p (@repinject CompSpecs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall (_ : @reptype CompSpecs t) (_ : val), mpred) (v : @reptype CompSpecs (Tarray t n a)) => @array_pred (@reptype CompSpecs t) (@Inhabitant_reptype CompSpecs t) Z0 (Z.max Z0 n) (fun (i : Z) (v0 : @reptype CompSpecs t) (v1 : val) => P v0 (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) t) i) v1)) (@unfold_reptype CompSpecs (Tarray t n a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tstruct id a)) => @aggregate_pred.auxiliary_pred.struct_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tunion id a)) => @aggregate_pred.auxiliary_pred.union_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tunion id a) v)) (@nested_field_type CompSpecs t_struct_foo (@cons gfield (StructField _x) (@nil gfield))) (Vint (Int.repr (Zpos (xI (xO xH))))) (offset_val (@nested_field_offset CompSpecs t_struct_foo (@cons gfield (StructField _x) (@nil gfield))) (gv _s)))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _y) (@nil gfield)) (gv _s))) (@type_induction.type_func CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) (fun (t : type) (v : @reptype CompSpecs t) (p : val) => if type_is_volatile t then memory_block Ews (@sizeof (@cenv_cs CompSpecs) t) p else mapsto Ews t p (@repinject CompSpecs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall (_ : @reptype CompSpecs t) (_ : val), mpred) (v : @reptype CompSpecs (Tarray t n a)) => @array_pred (@reptype CompSpecs t) (@Inhabitant_reptype CompSpecs t) Z0 (Z.max Z0 n) (fun (i : Z) (v0 : @reptype CompSpecs t) (v1 : val) => P v0 (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) t) i) v1)) (@unfold_reptype CompSpecs (Tarray t n a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tstruct id a)) => @aggregate_pred.auxiliary_pred.struct_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tunion id a)) => @aggregate_pred.auxiliary_pred.union_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tunion id a) v)) (@nested_field_type CompSpecs t_struct_foo (@cons gfield (StructField _y) (@nil gfield))) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (offset_val (@nested_field_offset CompSpecs t_struct_foo (@cons gfield (StructField _y) (@nil gfield))) (gv _s))))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _z) (@nil gfield)) (gv _s))) (@type_induction.type_func CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) (fun (t : type) (v : @reptype CompSpecs t) (p : val) => if type_is_volatile t then memory_block Ews (@sizeof (@cenv_cs CompSpecs) t) p else mapsto Ews t p (@repinject CompSpecs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall (_ : @reptype CompSpecs t) (_ : val), mpred) (v : @reptype CompSpecs (Tarray t n a)) => @array_pred (@reptype CompSpecs t) (@Inhabitant_reptype CompSpecs t) Z0 (Z.max Z0 n) (fun (i : Z) (v0 : @reptype CompSpecs t) (v1 : val) => P v0 (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) t) i) v1)) (@unfold_reptype CompSpecs (Tarray t n a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tstruct id a)) => @aggregate_pred.auxiliary_pred.struct_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tunion id a)) => @aggregate_pred.auxiliary_pred.union_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tunion id a) v)) (@nested_field_type CompSpecs t_struct_foo (@cons gfield (StructField _z) (@nil gfield))) (Vfloat (Float.of_bits (Int64.repr Z0))) (offset_val (@nested_field_offset CompSpecs t_struct_foo (@cons gfield (StructField _z) (@nil gfield))) (gv _s))))) *)
simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs tuint (@nil gfield) (gv _s))) (@type_induction.type_func CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) (fun (t : type) (v : @reptype CompSpecs t) (p : val) => if type_is_volatile t then memory_block Ews (@sizeof (@cenv_cs CompSpecs) t) p else mapsto Ews t p (@repinject CompSpecs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall (_ : @reptype CompSpecs t) (_ : val), mpred) (v : @reptype CompSpecs (Tarray t n a)) => @array_pred (@reptype CompSpecs t) (@Inhabitant_reptype CompSpecs t) Z0 (Z.max Z0 n) (fun (i : Z) (v0 : @reptype CompSpecs t) (v1 : val) => P v0 (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) t) i) v1)) (@unfold_reptype CompSpecs (Tarray t n a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tstruct id a)) => @aggregate_pred.auxiliary_pred.struct_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tunion id a)) => @aggregate_pred.auxiliary_pred.union_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tunion id a) v)) (@nested_field_type CompSpecs tuint (@nil gfield)) (Vint (Int.repr (Zpos (xI (xO xH))))) (offset_val (@nested_field_offset CompSpecs tuint (@nil gfield)) (gv _s))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _x) (@nil gfield)) (gv _s))) (@type_induction.type_func CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) (fun (t : type) (v : @reptype CompSpecs t) (p : val) => if type_is_volatile t then memory_block Ews (@sizeof (@cenv_cs CompSpecs) t) p else mapsto Ews t p (@repinject CompSpecs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall (_ : @reptype CompSpecs t) (_ : val), mpred) (v : @reptype CompSpecs (Tarray t n a)) => @array_pred (@reptype CompSpecs t) (@Inhabitant_reptype CompSpecs t) Z0 (Z.max Z0 n) (fun (i : Z) (v0 : @reptype CompSpecs t) (v1 : val) => P v0 (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) t) i) v1)) (@unfold_reptype CompSpecs (Tarray t n a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tstruct id a)) => @aggregate_pred.auxiliary_pred.struct_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tunion id a)) => @aggregate_pred.auxiliary_pred.union_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tunion id a) v)) (@nested_field_type CompSpecs t_struct_foo (@cons gfield (StructField _x) (@nil gfield))) (Vint (Int.repr (Zpos (xI (xO xH))))) (offset_val (@nested_field_offset CompSpecs t_struct_foo (@cons gfield (StructField _x) (@nil gfield))) (gv _s)))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _y) (@nil gfield)) (gv _s))) (@type_induction.type_func CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) (fun (t : type) (v : @reptype CompSpecs t) (p : val) => if type_is_volatile t then memory_block Ews (@sizeof (@cenv_cs CompSpecs) t) p else mapsto Ews t p (@repinject CompSpecs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall (_ : @reptype CompSpecs t) (_ : val), mpred) (v : @reptype CompSpecs (Tarray t n a)) => @array_pred (@reptype CompSpecs t) (@Inhabitant_reptype CompSpecs t) Z0 (Z.max Z0 n) (fun (i : Z) (v0 : @reptype CompSpecs t) (v1 : val) => P v0 (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) t) i) v1)) (@unfold_reptype CompSpecs (Tarray t n a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tstruct id a)) => @aggregate_pred.auxiliary_pred.struct_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tunion id a)) => @aggregate_pred.auxiliary_pred.union_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tunion id a) v)) (@nested_field_type CompSpecs t_struct_foo (@cons gfield (StructField _y) (@nil gfield))) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (offset_val (@nested_field_offset CompSpecs t_struct_foo (@cons gfield (StructField _y) (@nil gfield))) (gv _s))))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _z) (@nil gfield)) (gv _s))) (@type_induction.type_func CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) (fun (t : type) (v : @reptype CompSpecs t) (p : val) => if type_is_volatile t then memory_block Ews (@sizeof (@cenv_cs CompSpecs) t) p else mapsto Ews t p (@repinject CompSpecs t v)) (fun (t : type) (n : Z) (a : attr) (P : forall (_ : @reptype CompSpecs t) (_ : val), mpred) (v : @reptype CompSpecs (Tarray t n a)) => @array_pred (@reptype CompSpecs t) (@Inhabitant_reptype CompSpecs t) Z0 (Z.max Z0 n) (fun (i : Z) (v0 : @reptype CompSpecs t) (v1 : val) => P v0 (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) t) i) v1)) (@unfold_reptype CompSpecs (Tarray t n a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tstruct id a)) => @aggregate_pred.auxiliary_pred.struct_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tstruct id a) v)) (fun (id : positive) (a : attr) (P : @type_induction.FT_aux CompSpecs (fun t : type => forall (_ : @reptype CompSpecs t) (_ : val), mpred) id) (v : @reptype CompSpecs (Tunion id a)) => @aggregate_pred.auxiliary_pred.union_data_at_rec_aux CompSpecs Ews (co_members (@get_co CompSpecs id)) (co_members (@get_co CompSpecs id)) (co_sizeof (@get_co CompSpecs id)) P (@unfold_reptype CompSpecs (Tunion id a) v)) (@nested_field_type CompSpecs t_struct_foo (@cons gfield (StructField _z) (@nil gfield))) (Vfloat (Float.of_bits (Int64.repr Z0))) (offset_val (@nested_field_offset CompSpecs t_struct_foo (@cons gfield (StructField _z) (@nil gfield))) (gv _s))))) *)
unfold field_at, data_at_rec, at_offset. simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs tuint (@nil gfield) (gv _s))) (mapsto Ews (Tint I32 Unsigned noattr) (offset_val Z0 (gv _s)) (Vint (Int.repr (Zpos (xI (xO xH)))))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _x) (@nil gfield)) (gv _s))) (mapsto Ews (Tint I32 Signed noattr) (offset_val Z0 (gv _s)) (Vint (Int.repr (Zpos (xI (xO xH))))))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _y) (@nil gfield)) (gv _s))) (mapsto Ews (Tfloat F32 noattr) (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_foo (@cons gfield (StructField _z) (@nil gfield)) (gv _s))) (mapsto Ews (Tfloat F64 noattr) (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))))) *)
  repeat (rewrite prop_true_andp by (auto with field_compatible)).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))))) (mapsto Ews (Tint I32 Unsigned noattr) (offset_val Z0 (gv _s)) (Vint (Int.repr (Zpos (xI (xO xH))))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews (Tint I32 Signed noattr) (offset_val Z0 (gv _s)) (Vint (Int.repr (Zpos (xI (xO xH)))))) (mapsto Ews (Tfloat F32 noattr) (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))))) (mapsto Ews (Tfloat F64 noattr) (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0))))) *)
fold noattr; fold tint; fold tfloat; fold tdouble.
repeat match goal with |- context [field_offset ?A ?B ?C] =>
  set (aa :=field_offset A B C); compute in aa; subst aa
end.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0)))) (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))))) (mapsto Ews (Tint I32 Unsigned noattr) (offset_val Z0 (gv _s)) (Vint (Int.repr (Zpos (xI (xO xH))))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mapsto Ews tint (offset_val Z0 (gv _s)) (Vint (Int.repr (Zpos (xI (xO xH)))))) (mapsto Ews tfloat (offset_val (Zpos (xO (xO xH))) (gv _s)) (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))))) (mapsto Ews tdouble (offset_val (Zpos (xO (xO (xO xH)))) (gv _s)) (Vfloat (Float.of_bits (Int64.repr Z0))))) *)
normalize. cancel.
}
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y1 (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons localdef (temp _y2 (force_val (sem_cast tfloat tint (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))))) (@cons localdef (temp _t'1 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (temp _x1 (Vint (Int.repr (Zpos (xI (xO xH)))))) (@cons localdef (temp _t'2 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (gvars gv) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y1 (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons localdef (temp _y2 (force_val (sem_cast tfloat tint (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))))) (@cons localdef (temp _t'1 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (temp _x1 (Vint (Int.repr (Zpos (xI (xO xH)))))) (@cons localdef (temp _t'2 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (gvars gv) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y1 (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons localdef (temp _y2 (force_val (sem_cast tfloat tint (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))))) (@cons localdef (temp _t'1 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (temp _x1 (Vint (Int.repr (Zpos (xI (xO xH)))))) (@cons localdef (temp _t'2 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (gvars gv) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y1 (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons localdef (temp _y2 (force_val (sem_cast tfloat tint (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))))) (@cons localdef (temp _t'1 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (temp _x1 (Vint (Int.repr (Zpos (xI (xO xH)))))) (@cons localdef (temp _t'2 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (gvars gv) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y1 (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons localdef (temp _y2 (force_val (sem_cast tfloat tint (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))))) (@cons localdef (temp _t'1 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (temp _x1 (Vint (Int.repr (Zpos (xI (xO xH)))))) (@cons localdef (temp _t'2 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (gvars gv) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y1 (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons localdef (temp _y2 (force_val (sem_cast tfloat tint (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))))) (@cons localdef (temp _t'1 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (temp _x1 (Vint (Int.repr (Zpos (xI (xO xH)))))) (@cons localdef (temp _t'2 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (gvars gv) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _y1 (Vfloat (Float.of_bits (Int64.repr Z0)))) (@cons localdef (temp _y2 (force_val (sem_cast tfloat tint (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))))) (@cons localdef (temp _t'1 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (temp _x1 (Vint (Int.repr (Zpos (xI (xO xH)))))) (@cons localdef (temp _t'2 (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))))) (@cons localdef (gvars gv) (@nil localdef))))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_foo (@pair val (prod val val) (Vint (Int.repr (Zpos (xI (xO xH))))) (@pair val val (Vsingle (Float32.of_bits (Int.repr (Zpos (xI (xO (xO (xO (xI (xI (xI (xO (xI (xO (xI (xI (xI (xI (xO (xO (xO (xI (xO (xI (xI (xO (xI (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))) (Vfloat (Float.of_bits (Int64.repr Z0))))) (gv _s)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.
Qed.
