From 6ee0923290cca4782e6c863d752fb74c2c01df4f Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 17 Dec 2021 14:28:00 +0100
Subject: fpdivu

---
 kvx/CBuiltins.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kvx/CBuiltins.ml')

diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml
index f2b7b09e..fad86d3c 100644
--- a/kvx/CBuiltins.ml
+++ b/kvx/CBuiltins.ml
@@ -136,7 +136,9 @@ let builtins = {
     "__builtin_lround_ne",
       (TInt(ILong, []), [TFloat(FDouble, [])], false);
     "__builtin_luround_ne",
-      (TInt(IULong, []), [TFloat(FDouble, [])], false);
+    (TInt(IULong, []), [TFloat(FDouble, [])], false);
+    "__builtin_fp_udiv32",
+    (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false);
 ]
 }
 
-- 
cgit