From 21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 18:53:04 +0100
Subject: bits to float

---
 riscV/CBuiltins.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'riscV/CBuiltins.ml')

diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index 55b6bbd5..00b44fd5 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -50,6 +50,10 @@ let builtins = {
       (TInt(IULong, []), [TFloat(FDouble, [])], false);
     "__builtin_bits_of_float",
       (TInt(IUInt, []), [TFloat(FFloat, [])], false);
+    "__builtin_double_of_bits",
+      (TFloat(FDouble, []), [TInt(IULong, [])], false);
+    "__builtin_float_of_bits",
+      (TFloat(FFloat, []), [TInt(IUInt, [])], false);
   ]
 }
 
-- 
cgit