From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Globalenvs.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'common/Globalenvs.v') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index bd38fa3..a34a05d 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -516,7 +516,7 @@ Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option m | Init_int16 n => Mem.store Mint16unsigned m b p (Vint n) | Init_int32 n => Mem.store Mint32 m b p (Vint n) | Init_int64 n => Mem.store Mint64 m b p (Vlong n) - | Init_float32 n => Mem.store Mfloat32 m b p (Vfloat n) + | Init_float32 n => Mem.store Mfloat32 m b p (Vsingle n) | Init_float64 n => Mem.store Mfloat64 m b p (Vfloat n) | Init_addrof symb ofs => match find_symbol ge symb with @@ -848,7 +848,7 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s Mem.load Mint64 m b p = Some(Vlong n) /\ load_store_init_data m b (p + 8) il' | Init_float32 n :: il' => - Mem.load Mfloat32 m b p = Some(Vfloat(Float.singleoffloat n)) + Mem.load Mfloat32 m b p = Some(Vsingle n) /\ load_store_init_data m b (p + 4) il' | Init_float64 n :: il' => Mem.load Mfloat64 m b p = Some(Vfloat n) @@ -895,7 +895,7 @@ Proof. eapply (A Mint16unsigned (Vint i)); eauto. eapply (A Mint32 (Vint i)); eauto. eapply (A Mint64 (Vlong i)); eauto. - eapply (A Mfloat32 (Vfloat f)); eauto. + eapply (A Mfloat32 (Vsingle f)); eauto. eapply (A Mfloat64 (Vfloat f)); eauto. inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0). eapply store_init_data_list_outside; eauto. right. simpl. xomega. -- cgit v1.2.3