diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 19:28:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 19:28:03 +0100 |
| commit | 50ea35fceb52c5f66ccbc4f709df3a3471b12647 (patch) | |
| tree | cbbe994acd0e7e50c8a0302c5b62c84b0e753709 /cfrontend/C2C.ml | |
| parent | 202050c6240a11c94cc8b6ab599022fee7bd2471 (diff) | |
| download | compcert-kvx-50ea35fceb52c5f66ccbc4f709df3a3471b12647.tar.gz compcert-kvx-50ea35fceb52c5f66ccbc4f709df3a3471b12647.zip | |
added helper functions but strange
idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 18 |
1 files changed, 17 insertions, 1 deletions
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); ] } |