diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 50 | ||||
-rw-r--r-- | cfrontend/PrintClight.ml | 2 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 2 |
3 files changed, 39 insertions, 15 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 2b9a54a4..4cb4ded6 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -199,6 +199,10 @@ let builtins_generic = { (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); + "__compcert_va_composite", + (TPtr(TVoid [], []), + [TPtr(TVoid [], []); TInt(IUInt, [])], + false); (* Helper functions for int64 arithmetic *) "__i64_dtos", (TInt(ILongLong, []), @@ -381,26 +385,46 @@ let va_list_ptr e = | Evalof(e', _) -> Eaddrof(e', Tpointer(typeof e, noattr)) | _ -> error "bad use of a va_list object"; e -let make_builtin_va_arg env ty e = - let (helper, ty_ret) = - match ty with - | Tint _ | Tpointer _ -> - ("__compcert_va_int32", Tint(I32, Unsigned, noattr)) - | Tlong _ -> - ("__compcert_va_int64", Tlong(Unsigned, noattr)) - | Tfloat _ -> - ("__compcert_va_float64", Tfloat(F64, noattr)) - | _ -> - unsupported "va_arg at this type"; - ("", Tvoid) in +let make_builtin_va_arg_by_val helper ty ty_ret arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in Ecast (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), - Econs(va_list_ptr e, Enil), + Econs(va_list_ptr arg, Enil), ty_ret), ty) +let make_builtin_va_arg_by_ref helper ty arg = + let ty_fun = + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), + Tpointer(Tvoid, noattr), cc_default) in + let ty_ptr = + Tpointer(ty, noattr) in + let call = + Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), + Econs(va_list_ptr arg, + Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)), + Tpointer(Tvoid, noattr)) in + Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) + +let make_builtin_va_arg env ty e = + match ty with + | Tint _ | Tpointer _ -> + make_builtin_va_arg_by_val + "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e + | Tlong _ -> + make_builtin_va_arg_by_val + "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e + | Tfloat _ -> + make_builtin_va_arg_by_val + "__compcert_va_float64" ty (Tfloat(F64, noattr)) e + | Tstruct _ | Tunion _ -> + make_builtin_va_arg_by_ref + "__compcert_va_composite" ty e + | _ -> + unsupported "va_arg at this type"; + Eval(Vint(coqint_of_camlint 0l), type_int32s) + (** ** Translation functions *) (** Constants *) diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ebd06c54..f1c3ef18 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -206,7 +206,7 @@ and print_cases p cases = and print_case_label p = function | None -> fprintf p "default" - | Some lbl -> fprintf p "case %ld" (camlint_of_coqint lbl) + | Some lbl -> fprintf p "case %s" (Z.to_string lbl) and print_stmt_for p s = match s with diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 8a4d60a5..882272b8 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -346,7 +346,7 @@ and print_cases p cases = and print_case_label p = function | None -> fprintf p "default" - | Some lbl -> fprintf p "case %ld" (camlint_of_coqint lbl) + | Some lbl -> fprintf p "case %s" (Z.to_string lbl) and print_stmt_for p s = match s with |