bits to float

1 files changed, 9 insertions, 1 deletions

diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
index 86bcb2ac..47bacffa 100644
--- a/riscV/Builtins1.v
+++ b/riscV/Builtins1.v
@@ -22,23 +22,31 @@ Require ExtValues.
 
 Inductive platform_builtin : Type :=
 | BI_bits_of_float
-| BI_bits_of_double.
+| BI_bits_of_double
+| BI_float_of_bits
+| BI_double_of_bits.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
      ("__builtin_bits_of_float", BI_bits_of_float)
   :: ("__builtin_bits_of_double", BI_bits_of_double)
+  :: ("__builtin_float_of_bits", BI_float_of_bits)
+  :: ("__builtin_double_of_bits", BI_double_of_bits)
   :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
   match b with
   | BI_bits_of_float => mksignature (Tsingle :: nil) Tint cc_default
   | BI_bits_of_double => mksignature (Tfloat :: nil) Tlong cc_default
+  | BI_float_of_bits => mksignature (Tint :: nil) Tsingle cc_default
+  | BI_double_of_bits => mksignature (Tlong :: nil) Tfloat cc_default
   end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
   match b with
   | BI_bits_of_float => mkbuiltin_n1t Tsingle Tint Float32.to_bits
   | BI_bits_of_double => mkbuiltin_n1t Tfloat Tlong Float.to_bits
+  | BI_float_of_bits => mkbuiltin_n1t Tint Tsingle Float32.of_bits
+  | BI_double_of_bits => mkbuiltin_n1t Tlong Tfloat Float.of_bits
   end.