From 50ea35fceb52c5f66ccbc4f709df3a3471b12647 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 19:28:03 +0100
Subject: added helper functions but strange idiv.c: error:
 __compcert_i32_sdiv: missing or incorrect declaration

---
 cfrontend/C2C.ml | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'cfrontend/C2C.ml')

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index d70c4dad..f928a5d3 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -294,7 +294,23 @@ let builtins_generic = {
     "__compcert_i64_umulh",
         (TInt(IULongLong, []),
          [TInt(IULongLong, []); TInt(IULongLong, [])],
-         false)
+         false);
+    "__compcert_i32_sdiv",
+        (TInt(IInt, []),
+         [TInt(IInt, []); TInt(IInt, [])],
+         false);
+    "__compcert_i32_udiv",
+        (TInt(IUInt, []),
+         [TInt(IUInt, []); TInt(IUInt, [])],
+         false);
+    "__compcert_i32_smod",
+        (TInt(IInt, []),
+         [TInt(IInt, []); TInt(IInt, [])],
+         false);
+    "__compcert_i32_umod",
+        (TInt(IUInt, []),
+         [TInt(IUInt, []); TInt(IUInt, [])],
+         false);
   ]
 }
 
-- 
cgit