diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:17:40 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:17:40 +0100 |
| commit | 1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68 (patch) | |
| tree | 210ffc156c83f04fb0c61a40b4f9037d7ba8a7e1 /cfrontend/C2C.ml | |
| parent | 222c9047d61961db9c6b19fed5ca49829223fd33 (diff) | |
| parent | 12be46d59a2483a10d77fa8ee67f7e0ca1bd702f (diff) | |
| download | compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.tar.gz compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.zip | |
Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 40 |
1 files changed, 36 insertions, 4 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 293e79f0..ec5fb4dc 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -164,7 +164,7 @@ let ais_annot_functions = true);] else [] - + let builtins_generic = { builtin_typedefs = []; builtin_functions = @@ -312,7 +312,31 @@ 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); + "__compcert_f32_div", + (TFloat(FFloat,[]), + [TFloat(FFloat,[]); TFloat(FFloat,[])], + false); + "__compcert_f64_div", + (TFloat(FDouble,[]), + [TFloat(FDouble,[]); TFloat(FDouble,[])], + false); ] } @@ -1248,7 +1272,10 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__compcert_i64_" +let re_runtime64 = Str.regexp "__compcert_i64" +let re_runtime32 = Str.regexp "__compcert_i32" +let re_runtimef32 = Str.regexp "__compcert_f32" +let re_runtimef64 = Str.regexp "__compcert_f64" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1261,7 +1288,12 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then AST.EF_malloc else if id.name = "free" then AST.EF_free else - if Str.string_match re_runtime id.name 0 then AST.EF_runtime(id'', sg) else + if Str.string_match re_runtime64 id.name 0 + || Str.string_match re_runtime32 id.name 0 + || Str.string_match re_runtimef64 id.name 0 + || Str.string_match re_runtimef32 id.name 0 + then AST.EF_runtime(id'', sg) + else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.builtin_functions then AST.EF_builtin(id'', sg) |