diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 11:23:52 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 11:23:52 +0000 |
| commit | 7a614ea53948423b0266eefd98ea5714559c3cfc (patch) | |
| tree | b590210c9db8a450bd16cece9311ca47f68d0b89 /lib/Floats.v | |
| parent | 5312915c1b29929f82e1f8de80609a277584913f (diff) | |
Changelog: updated
driver/Interp.ml: clean up dead code
lib/Integers.v: add shifted_or_is_add
lib/Floats.v: add from_words_eq
.depend: updated
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Floats.v')
| -rw-r--r-- | lib/Floats.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index e7a7aa0..edb6d6b 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -189,6 +189,20 @@ Definition from_words (hi lo: int) : float := (Int64.or (Int64.shl (Int64.repr (Int.unsigned hi)) (Int64.repr 32)) (Int64.repr (Int.unsigned lo))). +Lemma from_words_eq: + forall lo hi, + from_words hi lo = + double_of_bits (Int64.repr (Int.unsigned hi * two_p 32 + Int.unsigned lo)). +Proof. + intros. unfold from_words. decEq. + rewrite Int64.shifted_or_is_add. + apply Int64.eqm_samerepr. auto with ints. + change (Z_of_nat Int64.wordsize) with 64. omega. + generalize (Int.unsigned_range lo). intros [A B]. + rewrite Int64.unsigned_repr. assumption. + assert (Int.modulus < Int64.max_unsigned). compute; auto. omega. +Qed. + (** Below are the only properties of floating-point arithmetic that we rely on in the compiler proof. *) |