remove singleoflongu (does not exist)

1 files changed, 9 insertions, 1 deletions

diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v
index 163dcbd8..9a04815b 100644
--- a/kvx/Builtins1.v
+++ b/kvx/Builtins1.v
@@ -28,7 +28,8 @@ Inductive platform_builtin : Type :=
 | BI_fmaf
 | BI_lround_ne
 | BI_luround_ne
-| BI_fp_udiv32.
+| BI_fp_udiv32
+| BI_fp_udiv64.
 
 Local Open Scope string_scope.
 
@@ -42,6 +43,7 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
   :: ("__builtin_lround_ne", BI_lround_ne)
   :: ("__builtin_luround_ne", BI_luround_ne)
   :: ("__builtin_fp_udiv32", BI_fp_udiv32)
+  :: ("__builtin_fp_udiv64", BI_fp_udiv64)
   :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
@@ -58,6 +60,8 @@ Definition platform_builtin_sig (b: platform_builtin) : signature :=
       mksignature (Tfloat :: nil) Tlong cc_default
   | BI_fp_udiv32 =>
       mksignature (Tint :: Tint :: nil) Tint cc_default
+  | BI_fp_udiv64 =>
+      mksignature (Tlong :: Tlong :: nil) Tlong cc_default
   end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
@@ -74,4 +78,8 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl
        (fun n1 n2 => if Int.eq n2 Int.zero
                      then None
                      else Some (Int.divu n1 n2))
+  | BI_fp_udiv64 => mkbuiltin_n2p Tlong Tlong Tlong
+       (fun n1 n2 => if Int64.eq n2 Int64.zero
+                     then None
+                     else Some (Int64.divu n1 n2))
   end.