Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 23 insertions, 0 deletions

diff --git a/caml/Floataux.ml b/caml/Floataux.ml
new file mode 100644
index 00000000..f43efa27
--- /dev/null
+++ b/caml/Floataux.ml
@@ -0,0 +1,23 @@
+open Camlcoq
+
+let singleoffloat f =
+  Int32.float_of_bits (Int32.bits_of_float f)
+
+let intoffloat f =
+  coqint_of_camlint (Int32.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
+  | AST.Ceq -> x = y
+  | AST.Cne -> x <> y
+  | AST.Clt -> x < y
+  | AST.Cle -> x <= y
+  | AST.Cgt -> x > y
+  | AST.Cge -> x >= y