diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
commit | 01e32a075023ce7b037d42d048b1904ba3d9a82b (patch) | |
tree | 2d01f3855234e6eb945b929e489232001c406592 /cfrontend/C2C.ml | |
parent | 093e0ea167fde39429bf4bd3fc693a232af0d093 (diff) | |
parent | 1fdca8371317e656cb08eaec3adb4596d6447e9b (diff) | |
download | compcert-01e32a075023ce7b037d42d048b1904ba3d9a82b.tar.gz compcert-01e32a075023ce7b037d42d048b1904ba3d9a82b.zip |
Merge branch 'master' into cleanup
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 6eabfbf4..16e8a80d 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1078,7 +1078,7 @@ let convertFundef loc env fd = a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; - (id', Gfun(Csyntax.Internal + (id', Gfun(Ctypes.Internal {fn_return = ret; fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; fn_params = params; @@ -1088,6 +1088,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) = @@ -1100,11 +1101,12 @@ 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) else EF_external(id'', sg) in - (id', Gfun(Csyntax.External(ef, args, res, cconv))) + (id', Gfun(Ctypes.External(ef, args, res, cconv))) (** Initializers *) |