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

1 files changed, 39 insertions, 0 deletions

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