From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 9 Feb 2006 14:55:48 +0000
Subject: Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/Floataux.ml | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 caml/Floataux.ml

(limited to 'caml/Floataux.ml')

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
-- 
cgit