From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Floataux.ml | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 lib/Floataux.ml (limited to 'lib/Floataux.ml') diff --git a/lib/Floataux.ml b/lib/Floataux.ml new file mode 100644 index 00000000..6b3b825f --- /dev/null +++ b/lib/Floataux.ml @@ -0,0 +1,39 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open Camlcoq +open Integers + +let singleoffloat f = + Int32.float_of_bits (Int32.bits_of_float f) + +let intoffloat f = + coqint_of_camlint (Int32.of_float f) + +let intuoffloat f = + coqint_of_camlint (Int64.to_int32 (Int64.of_float f)) + +let floatofint i = + Int32.to_float (camlint_of_coqint i) + +let floatofintu i = + Int64.to_float (Int64.logand (Int64.of_int32 (camlint_of_coqint i)) + 0xFFFFFFFFL) + +let cmp c (x: float) (y: float) = + match c with + | Ceq -> x = y + | Cne -> x <> y + | Clt -> x < y + | Cle -> x <= y + | Cgt -> x > y + | Cge -> x >= y -- cgit