diff options
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 94f13aa1..71328c71 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -437,10 +437,10 @@ 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 attr = +let convertCallconv va unproto attr = let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in - { cc_vararg = va; cc_structret = sr <> [] } + { cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } (** Types *) @@ -494,7 +494,7 @@ let rec convertTyp env t = | Some tl -> convertParams env tl end, convertTyp env tres, - convertCallconv va a) + convertCallconv va (targs = None) a) | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> @@ -626,7 +626,6 @@ let ewrap = function error ("retyping error: " ^ string_of_errmsg msg); ezero let rec convertExpr env e = - (*let ty = convertTyp env e.etyp in*) match e.edesc with | C.EVar _ | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) @@ -734,9 +733,8 @@ let rec convertExpr env e = ewrap (Ctyping.eseqor (convertExpr env e1) (convertExpr env e2)) | C.EConditional(e1, e2, e3) -> - ewrap (Ctyping.econdition' (convertExpr env e1) - (convertExpr env e2) (convertExpr env e3) - (convertTyp env e.etyp)) + ewrap (Ctyping.econdition (convertExpr env e1) + (convertExpr env e2) (convertExpr env e3)) | C.ECast(ty1, e1) -> ewrap (Ctyping.ecast (convertTyp env ty1) (convertExpr env e1)) | C.ECompound(ty1, ie) -> @@ -798,7 +796,8 @@ let rec convertExpr env e = let targs = convertTypArgs env [] args and tres = convertTyp env e.etyp in let sg = - signature_of_type targs tres {cc_vararg = true; cc_structret = false} in + signature_of_type targs tres + {cc_vararg = true; cc_unproto = false; cc_structret = false} in Ebuiltin(EF_external(intern_string "printf", sg), targs, convertExprList env args, tres) @@ -847,7 +846,7 @@ let convertAsm loc env txt outputs inputs clobber = let (txt', output', inputs') = ExtendedAsm.transf_asm loc env txt outputs inputs clobber in let clobber' = - List.map intern_string clobber in + List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in let ty_res = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) @@ -1033,11 +1032,12 @@ 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(Internal {fn_return = ret; - fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib; - fn_params = params; - fn_vars = vars; - fn_body = body'})) + (id', Gfun(Internal + {fn_return = ret; + fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; + fn_params = params; + fn_vars = vars; + fn_body = body'})) (** External function declaration *) |