diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 10:38:23 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 10:38:23 +0100 |
| commit | c86388b548984dae5f8dd794cad1f4b4505d4307 (patch) | |
| tree | 16b8344e8a4cb9f4d660f968cedd11f9acfa1305 /cfrontend/C2C.ml | |
| parent | 5ddc6e1de69aeeb1b03f4e495c8b75c2feec590d (diff) | |
| download | compcert-kvx-c86388b548984dae5f8dd794cad1f4b4505d4307.tar.gz compcert-kvx-c86388b548984dae5f8dd794cad1f4b4505d4307.zip | |
ça semble passer
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f928a5d3..f0ae4367 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1214,7 +1214,7 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__compcert_i64_" +let re_runtime = Str.regexp "__compcert_i" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1227,7 +1227,9 @@ 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_runtime 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.Builtins.functions then AST.EF_builtin(id'', sg) |