diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 12:55:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 12:55:03 +0100 |
| commit | 2638a022276c932ed00dc3f64b0e58bc0114a3d7 (patch) | |
| tree | bc8beeb8f99d55ac3bf7012e858a0fae2d38bc31 /cfrontend | |
| parent | 3718f2f520fc9a4dec2e9c1ac6eaf71f36f4f8a1 (diff) | |
| download | compcert-kvx-2638a022276c932ed00dc3f64b0e58bc0114a3d7.tar.gz compcert-kvx-2638a022276c932ed00dc3f64b0e58bc0114a3d7.zip | |
la division flottante fonctionne
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f0ae4367..bd9b7487 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -311,6 +311,14 @@ let builtins_generic = { (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); ] } @@ -1214,7 +1222,10 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__compcert_i" +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) = @@ -1227,7 +1238,10 @@ 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 + 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 |