diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-10-27 16:26:08 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-10-27 16:26:08 +0200 |
commit | 9922feea537ced718a3822dd50eabc87da060338 (patch) | |
tree | 6f67bb6707ef59e50d6bb81c61b2ed0b3c6097ab /arm/Archi.v | |
parent | f2d6637c7d4a11f961ff289e64f70bf4de93d0aa (diff) | |
parent | d50773e537ec6729f9152b545c6f938ab19eb7b8 (diff) | |
download | compcert-9922feea537ced718a3822dd50eabc87da060338.tar.gz compcert-9922feea537ced718a3822dd50eabc87da060338.zip |
Merge pull request #145 from AbsInt/64
Support for 64-bit target processors + support for x86 in 64-bit mode
Diffstat (limited to 'arm/Archi.v')
-rw-r--r-- | arm/Archi.v | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/arm/Archi.v b/arm/Archi.v index fedc55f5..64afb3ec 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -20,10 +20,19 @@ Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. +Definition ptr64 := false. + Parameter big_endian: bool. -Notation align_int64 := 8%Z (only parsing). -Notation align_float64 := 8%Z (only parsing). +Definition align_int64 := 8%Z. +Definition align_float64 := 8%Z. + +Definition splitlong := true. + +Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. +Proof. + unfold splitlong, ptr64; congruence. +Qed. Program Definition default_pl_64 : bool * nan_pl 53 := (false, iter_nat 51 _ xO xH). @@ -45,7 +54,8 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p Definition float_of_single_preserves_sNaN := false. -Global Opaque default_pl_64 choose_binop_pl_64 +Global Opaque ptr64 big_endian splitlong + default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. |