diff options
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d830ada6..61172dda 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -590,10 +590,16 @@ let convertAttr a = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } -let convertCallconv va unproto attr = +let convertCallconv _tres targs va attr = + let vararg = + match targs with + | None -> None + | Some tl -> if va then Some (Z.of_uint (List.length tl)) else None in let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in - { AST.cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } + { AST.cc_vararg = vararg; + AST.cc_unproto = (targs = None); + AST.cc_structret = (sr <> []) } (** Types *) @@ -661,7 +667,7 @@ let rec convertTyp env t = | Some tl -> convertParams env tl end, convertTyp env tres, - convertCallconv va (targs = None) a) + convertCallconv tres targs va a) | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> @@ -1035,7 +1041,7 @@ let rec convertExpr env e = and tres = convertTyp env e.etyp in let sg = signature_of_type targs tres - { AST.cc_vararg = true; cc_unproto = false; cc_structret = false} in + { AST.cc_vararg = Some (coqint_of_camlint 1l); cc_unproto = false; cc_structret = false} in Ebuiltin( AST.EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) @@ -1303,7 +1309,8 @@ let convertFundef loc env fd = a_loc = loc }; (id', AST.Gfun(Ctypes.Internal {fn_return = ret; - fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; + fn_callconv = convertCallconv fd.fd_ret (Some fd.fd_params) + fd.fd_vararg fd.fd_attrib; fn_params = params; fn_vars = vars; fn_body = body'})) @@ -1382,8 +1389,13 @@ let convertGlobvar loc env (sto, id, ty, optinit) = then [] else [AST.Init_space sz] | Some i -> convertInitializer env ty i in + let initialized = + if optinit = None then Sections.Uninit else + if List.exists (function AST.Init_addrof _ -> true | _ -> false) init' + then Sections.Init_reloc + else Sections.Init in let (section, access) = - Sections.for_variable env loc id' ty (optinit <> None) + Sections.for_variable env loc id' ty initialized (match sto with | Storage_thread_local | Storage_thread_local_extern | Storage_thread_local_static -> true |