diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 10:23:18 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 10:23:18 +0100 |
| commit | 2b5f5cb0bb6d8dbf302ab6d84c27eda30252912d (patch) | |
| tree | aea549d4f8a35fe5ca70a4eb7c21c2bafdc9781d /cfrontend/C2C.ml | |
| parent | be2315351761e4fc0430b91ac791d66eec0e0cd7 (diff) | |
| download | compcert-2b5f5cb0bb6d8dbf302ab6d84c27eda30252912d.tar.gz compcert-2b5f5cb0bb6d8dbf302ab6d84c27eda30252912d.zip | |
Add support for EF_runtime externals
Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index e4001e6b..418fa702 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1090,6 +1090,7 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" +let re_runtime = Str.regexp "__i64_" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1102,6 +1103,7 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then EF_malloc else if id.name = "free" then EF_free else + if Str.string_match re_runtime id.name 0 then EF_runtime(id'', sg) else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.functions then EF_builtin(id'', sg) |