diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
| commit | 2a0168fea37b68ad14e2cb60bf215111e49d4870 (patch) | |
| tree | 2f59373790d8ce3a5df66ef7a692271cf0666c6c /common/Globalenvs.v | |
| parent | 00805153cf9b88aa07cc6694b17d93f5ba2e7de8 (diff) | |
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
Diffstat (limited to 'common/Globalenvs.v')
| -rw-r--r-- | common/Globalenvs.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |