diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 161 | ||||
| -rw-r--r-- | cfrontend/CPragmas.ml | 5 | ||||
| -rw-r--r-- | cfrontend/PrintClight.ml | 13 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 18 |
4 files changed, 101 insertions, 96 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 439cc584..6a33c48d 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -13,20 +13,13 @@ (* *) (* *********************************************************************) -open Printf - open C -open Env -open Builtins open Camlcoq -open AST -open Values -open !Ctypes -open !Cop -open !Csyntax -open !Initializers open Floats +open Values +open Ctypes +open Csyntax (** ** Extracting information about global variables from their atom *) @@ -114,8 +107,8 @@ let currentLocation = ref Cutil.no_loc let updateLoc l = currentLocation := l -let error msg = - Cerrors.error !currentLocation "%s" msg +let error fmt = + Cerrors.error !currentLocation fmt let unsupported msg = Cerrors.error !currentLocation "unsupported feature: %s" msg @@ -133,8 +126,8 @@ let string_of_errmsg msg = (** ** The builtin environment *) let builtins_generic = { - typedefs = []; - functions = [ + Builtins.typedefs = []; + Builtins.functions = [ (* Floating-point absolute value *) "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); @@ -266,8 +259,22 @@ let builtins_generic = { (* Add processor-dependent builtins *) let builtins = - { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; - functions = builtins_generic.functions @ CBuiltins.builtins.functions } + Builtins.({ typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; + functions = builtins_generic.Builtins.functions @ CBuiltins.builtins.functions }) + +(** ** The known attributes *) + +let attributes = [ + (* type-related *) + ("aligned", Cutil.Attr_type); + (* struct-related *) + ("packed", Cutil.Attr_struct); + (* function-related *) + ("noreturn", Cutil.Attr_function); + (* name-related *) + ("section", Cutil.Attr_name) +] + (** ** Functions used to handle string literals *) @@ -302,8 +309,8 @@ let global_for_string s id = init := AST.Init_int8(Z.of_uint(Char.code c)) :: !init in add_char '\000'; for i = String.length s - 1 downto 0 do add_char s.[i] done; - (id, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init; - gvar_readonly = true; gvar_volatile = false}) + (id, AST.Gvar { AST.gvar_info = typeStringLiteral s; AST.gvar_init = !init; + AST.gvar_readonly = true; AST.gvar_volatile = false}) let name_for_wide_string_literal s = try @@ -343,7 +350,7 @@ let global_for_wide_string s id = init := init_of_char(Z.of_uint64 c) :: !init in List.iter add_char s; add_char 0L; - (id, Gvar {gvar_info = typeWideStringLiteral s; gvar_init = List.rev !init; + AST.(id, Gvar { gvar_info = typeWideStringLiteral s; gvar_init = List.rev !init; gvar_readonly = true; gvar_volatile = false}) let globals_for_strings globs = @@ -381,7 +388,7 @@ let make_builtin_memcpy args = if not (Z.eq (Z.modulo sz1 al1) Z.zero) then error "alignment argument of '__builtin_memcpy_aligned' must be a divisor of the size"; (* Issue #28: must decay array types to pointer types *) - Ebuiltin(EF_memcpy(sz1, al1), + Ebuiltin( AST.EF_memcpy(sz1, al1), Tcons(typeconv(typeof dst), Tcons(typeconv(typeof src), Tnil)), Econs(dst, Econs(src, Enil)), Tvoid) @@ -398,7 +405,7 @@ let va_list_ptr e = 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 + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, AST.cc_default) in Ecast (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), Econs(va_list_ptr arg, Enil), @@ -408,7 +415,7 @@ let make_builtin_va_arg_by_val helper ty ty_ret arg = let make_builtin_va_arg_by_ref helper ty arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tcons(Ctyping.size_t, Tnil)), - Tpointer(Tvoid, noattr), cc_default) in + Tpointer(Tvoid, noattr), AST.cc_default) in let ty_ptr = Tpointer(ty, noattr) in let call = @@ -460,13 +467,13 @@ let convertAttr a = let convertCallconv va unproto attr = let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in - { cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } + { AST.cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } (** Types *) let convertIkind k a : coq_type = match k with - | C.IBool -> Tint (IBool, Unsigned, a) + | C.IBool -> Tint (Ctypes.IBool, Unsigned, a) | C.IChar -> Tint (I8, (if Machine.((!config).char_signed) then Signed else Unsigned), a) | C.ISChar -> Tint (I8, Signed, a) @@ -532,7 +539,7 @@ let rec convertTyp env t = | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> - Tstruct(intern_string id.name, convertAttr a) + Ctypes.Tstruct(intern_string id.name, convertAttr a) | C.TUnion(id, a) -> Tunion(intern_string id.name, convertAttr a) | C.TEnum(id, a) -> @@ -565,7 +572,7 @@ let convertCompositedef env su id attr members = | C.Union -> TUnion (id,attr) in Debug.set_composite_size id su (Cutil.sizeof env t); Composite(intern_string id.name, - begin match su with C.Struct -> Struct | C.Union -> Union end, + begin match su with C.Struct -> Ctypes.Struct | C.Union -> Ctypes.Union end, List.map (convertField env) members, convertAttr attr) @@ -660,7 +667,7 @@ let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) let ewrap = function | Errors.OK e -> e | Errors.Error msg -> - error ("retyping error: " ^ string_of_errmsg msg); ezero + error "retyping error: %s" (string_of_errmsg msg); ezero let rec convertExpr env e = match e.edesc with @@ -693,13 +700,13 @@ let rec convertExpr env e = Ctyping.ealignof (convertTyp env ty1) | C.EUnop(C.Ominus, e1) -> - ewrap (Ctyping.eunop Oneg (convertExpr env e1)) + ewrap (Ctyping.eunop Cop.Oneg (convertExpr env e1)) | C.EUnop(C.Oplus, e1) -> convertExpr env e1 | C.EUnop(C.Olognot, e1) -> - ewrap (Ctyping.eunop Onotbool (convertExpr env e1)) + ewrap (Ctyping.eunop Cop.Onotbool (convertExpr env e1)) | C.EUnop(C.Onot, e1) -> - ewrap (Ctyping.eunop Onotint (convertExpr env e1)) + ewrap (Ctyping.eunop Cop.Onotint (convertExpr env e1)) | C.EUnop(C.Oaddrof, e1) -> ewrap (Ctyping.eaddrof (convertLvalue env e1)) | C.EUnop(C.Opreincr, e1) -> @@ -793,7 +800,7 @@ let rec convertExpr env e = | [] -> assert false (* catched earlier *) in let targs2 = convertTypArgs env [] args2 in Ebuiltin( - EF_debug(P.of_int64 kind, intern_string text, + AST.EF_debug(P.of_int64 kind, intern_string text, typlist_of_typelist targs2), targs2, convertExprList env args2, convertTyp env e.etyp) @@ -802,7 +809,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), + AST.EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "argument 1 of '__builtin_annot' must be a string literal"; @@ -814,7 +821,7 @@ let rec convertExpr env e = | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in - Ebuiltin(EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), + Ebuiltin(AST.EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> @@ -826,7 +833,7 @@ let rec convertExpr env e = make_builtin_memcpy (convertExprList env args) | C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) -> - ewrap (Ctyping.eunop Oabsfloat (convertExpr env arg)) + ewrap (Ctyping.eunop Cop.Oabsfloat (convertExpr env arg)) | C.ECall({edesc = C.EVar {name = "__builtin_va_start"}} as fn, [arg]) -> Ecall(convertExpr env fn, @@ -842,7 +849,7 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_va_copy"}}, [arg1; arg2]) -> let dst = convertExpr env arg1 in let src = convertExpr env arg2 in - Ebuiltin(EF_memcpy(Z.of_uint CBuiltins.size_va_list, Z.of_uint 4), + Ebuiltin( AST.EF_memcpy(Z.of_uint CBuiltins.size_va_list, Z.of_uint 4), Tcons(Tpointer(Tvoid, noattr), Tcons(Tpointer(Tvoid, noattr), Tnil)), Econs(va_list_ptr dst, Econs(va_list_ptr src, Enil)), @@ -854,8 +861,8 @@ let rec convertExpr env e = and tres = convertTyp env e.etyp in let sg = signature_of_type targs tres - {cc_vararg = true; cc_unproto = false; cc_structret = false} in - Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), + { AST.cc_vararg = true; cc_unproto = false; cc_structret = false} in + Ebuiltin( AST.EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) | C.ECall(fn, args) -> @@ -886,7 +893,7 @@ and convertLvalue env e = ewrap (Ctyping.efield !comp_env e3' (intern_string id)) | C.EBinop(C.Oindex, e1, e2, _) -> let e1' = convertExpr env e1 and e2' = convertExpr env e2 in - let e3' = ewrap (Ctyping.ebinop Oadd e1' e2') in + let e3' = ewrap (Ctyping.ebinop Cop.Oadd e1' e2') in ewrap (Ctyping.ederef e3') | _ -> error "illegal lvalue"; ezero @@ -909,8 +916,8 @@ let convertAsm loc env txt outputs inputs clobber = let e = let tinputs = convertTypArgs env [] inputs' in let toutput = convertTyp env ty_res in - Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', - signature_of_type tinputs toutput cc_default, + Ebuiltin( AST.EF_inline_asm(coqstring_of_camlstring txt', + signature_of_type tinputs toutput AST.cc_default, clobber'), tinputs, convertExprList env inputs', @@ -982,7 +989,7 @@ let rec contains_case s = let swrap = function | Errors.OK s -> s | Errors.Error msg -> - error ("retyping error: " ^ string_of_errmsg msg); Csyntax.Sskip + error "retyping error: %s" (string_of_errmsg msg); Csyntax.Sskip let rec convertStmt env s = updateLoc s.sloc; @@ -1010,9 +1017,9 @@ let rec convertStmt env s = (convertStmt env s1) te (convertStmt env s2) (convertStmt env s3)) | C.Sbreak -> - Sbreak + Csyntax.Sbreak | C.Scontinue -> - Scontinue + Csyntax.Scontinue | C.Sswitch(e, s1) -> let (init, cases) = groupSwitch (flattenSwitch s1) in let rec init_debug s = @@ -1029,25 +1036,25 @@ let rec convertStmt env s = swrap (Ctyping.sswitch te (convertSwitch env (is_int64 env e.etyp) cases)) | C.Slabeled(C.Slabel lbl, s1) -> - Slabel(intern_string lbl, convertStmt env s1) + Csyntax.Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> - unsupported "'case' statement not in 'switch' statement"; Sskip + unsupported "'case' statement not in 'switch' statement"; Csyntax.Sskip | C.Slabeled(C.Sdefault, _) -> - unsupported "'default' statement not in 'switch' statement"; Sskip + unsupported "'default' statement not in 'switch' statement"; Csyntax.Sskip | C.Sgoto lbl -> - Sgoto(intern_string lbl) + Csyntax.Sgoto(intern_string lbl) | C.Sreturn None -> - Sreturn None + Csyntax.Sreturn None | C.Sreturn(Some e) -> - Sreturn(Some(convertExpr env e)) + Csyntax.Sreturn(Some(convertExpr env e)) | C.Sblock _ -> - unsupported "nested blocks"; Sskip + unsupported "nested blocks"; Csyntax.Sskip | C.Sdecl _ -> - unsupported "inner declarations"; Sskip + unsupported "inner declarations"; Csyntax.Sskip | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option [-finline-asm])"; - Sdo (convertAsm s.sloc env txt outputs inputs clobber) + Csyntax.Sdo (convertAsm s.sloc env txt outputs inputs clobber) and convertSwitch env is_64 = function | [] -> @@ -1100,11 +1107,11 @@ let convertFundef loc env fd = Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; - a_sections = Sections.for_function env id' fd.fd_ret; + a_sections = Sections.for_function env id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; - (id', Gfun(Ctypes.Internal + (id', AST.Gfun(Ctypes.Internal {fn_return = ret; fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; fn_params = params; @@ -1125,14 +1132,14 @@ let convertFundecl env (sto, id, ty, optinit) = let id'' = coqstring_of_camlstring id.name in let sg = signature_of_type args res cconv in 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 id.name = "malloc" then AST.EF_malloc else + if id.name = "free" then AST.EF_free else + if Str.string_match re_runtime id.name 0 then AST.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(Ctypes.External(ef, args, res, cconv))) + && List.mem_assoc id.name builtins.Builtins.functions + then AST.EF_builtin(id'', sg) + else AST.EF_external(id'', sg) in + (id', AST.Gfun(Ctypes.External(ef, args, res, cconv))) (** Initializers *) @@ -1141,16 +1148,16 @@ let rec convertInit env init = | C.Init_single e -> Initializers.Init_single (convertExpr env e) | C.Init_array il -> - Initializers.Init_array (convertInitList env (List.rev il) Init_nil) + Initializers.Init_array (convertInitList env (List.rev il) Initializers.Init_nil) | C.Init_struct(_, flds) -> - Initializers.Init_struct (convertInitList env (List.rev_map snd flds) Init_nil) + Initializers.Init_struct (convertInitList env (List.rev_map snd flds) Initializers.Init_nil) | C.Init_union(_, fld, i) -> Initializers.Init_union (intern_string fld.fld_name, convertInit env i) and convertInitList env il accu = match il with | [] -> accu - | i :: il' -> convertInitList env il' (Init_cons(convertInit env i, accu)) + | i :: il' -> convertInitList env il' (Initializers.Init_cons(convertInit env i, accu)) let convertInitializer env ty i = match Initializers.transl_init @@ -1158,8 +1165,8 @@ let convertInitializer env ty i = with | Errors.OK init -> init | Errors.Error msg -> - error (sprintf "initializer element is not a compile-time constant (%s)" - (string_of_errmsg msg)); [] + error "initializer element is not a compile-time constant (%s)" + (string_of_errmsg msg); [] (** Global variable *) @@ -1173,16 +1180,16 @@ let convertGlobvar loc env (sto, id, ty, optinit) = let init' = match optinit with | None -> - if sto = C.Storage_extern then [] else [Init_space sz] + if sto = C.Storage_extern then [] else [AST.Init_space sz] | Some i -> convertInitializer env ty i in let (section, access) = Sections.for_variable env id' ty (optinit <> None) in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then - error (sprintf "'%s' is too big (%s bytes)" - id.name (Z.to_string sz)); + error "'%s' is too big (%s bytes)" + id.name (Z.to_string sz); if sto <> C.Storage_extern && Cutil.incomplete_type env ty then - error (sprintf "'%s' has incomplete type" id.name); + error "'%s' has incomplete type" id.name; Hashtbl.add decl_atom id' { a_storage = sto; a_alignment = Some (Z.to_int al); @@ -1192,7 +1199,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = a_loc = loc }; let volatile = List.mem C.AVolatile attr in let readonly = List.mem C.AConst attr && not volatile in - (id', Gvar {gvar_info = ty'; gvar_init = init'; + (id', AST.Gvar { AST.gvar_info = ty'; gvar_init = init'; gvar_readonly = readonly; gvar_volatile = volatile}) (** Convert a list of global declarations. @@ -1257,7 +1264,7 @@ let rec translEnv env = function | C.Gtypedef(id, ty) -> Env.add_typedef env id ty | C.Genumdef(id, attr, members) -> - Env.add_enum env id {ei_members = members; ei_attr = attr} + Env.add_enum env id {Env.ei_members = members; ei_attr = attr} | _ -> env in translEnv env' gl @@ -1277,13 +1284,13 @@ let cleanupGlobals p = match g.gdesc with | C.Gfundef fd -> if IdentSet.mem fd.fd_name !strong then - error ("multiple definitions of " ^ fd.fd_name.name); + error "multiple definitions of %s" fd.fd_name.name; strong := IdentSet.add fd.fd_name !strong | C.Gdecl(Storage_extern, id, ty, init) -> extern := IdentSet.add id !extern | C.Gdecl(sto, id, ty, Some i) -> if IdentSet.mem id !strong then - error ("multiple definitions of " ^ id.name); + error "multiple definitions of %s" id.name; strong := IdentSet.add id !strong | C.Gdecl(sto, id, ty, None) -> weak := IdentSet.add id !weak @@ -1334,8 +1341,8 @@ let convertProgram p = let typs = convertCompositedefs env [] p in match build_composite_env typs with | Errors.Error msg -> - error (sprintf "incorrect struct or union definition: %s" - (string_of_errmsg msg)); + error "incorrect struct or union definition: %s" + (string_of_errmsg msg); None | Errors.OK ce -> comp_env := ce; @@ -1350,4 +1357,4 @@ let convertProgram p = prog_comp_env = ce } in if Cerrors.check_errors () then None else Some p' with Env.Error msg -> - error (Env.error_message msg); None + error "%s" (Env.error_message msg); None diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index 2a199ff8..d61af920 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -15,7 +15,6 @@ (* Handling of pragmas *) -open Printf open Camlcoq (* #pragma section *) @@ -43,9 +42,9 @@ let re_c_ident = Str.regexp "[A-Za-z_][A-Za-z_0-9]*$" let process_use_section_pragma classname id = if id = "," || id = ";" then () else begin if not (Str.string_match re_c_ident id 0) then - C2C.error (sprintf "bad identifier `%s' in #pragma use_section" id); + C2C.error "bad identifier `%s' in #pragma use_section" id; if not (Sections.use_section_for (intern_string id) classname) then - C2C.error (sprintf "unknown section name `%s'" classname) + C2C.error "unknown section name `%s'" classname end (* #pragma reserve_register *) diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 7fa35f16..ecfaf0df 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -17,16 +17,15 @@ open Format open Camlcoq -open AST open PrintAST -open !Ctypes +open Ctypes open Cop open PrintCsyntax -open !Clight +open Clight (* Naming temporaries *) -let temp_name (id: ident) = "$" ^ Z.to_string (Z.Zpos id) +let temp_name (id: AST.ident) = "$" ^ Z.to_string (Z.Zpos id) (* Declarator (identifier + type) -- reuse from PrintCsyntax *) @@ -254,7 +253,7 @@ let print_function p id f = let print_fundef p id fd = match fd with - | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) -> + | Ctypes.External((AST.EF_external _ | AST.EF_runtime _), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) | Ctypes.External(_, _, _, _) -> @@ -264,8 +263,8 @@ let print_fundef p id fd = let print_globdef p (id, gd) = match gd with - | Gfun f -> print_fundef p id f - | Gvar v -> print_globvar p id v (* from PrintCsyntax *) + | AST.Gfun f -> print_fundef p id f + | AST.Gvar v -> print_globvar p id v (* from PrintCsyntax *) let print_program p prog = fprintf p "@[<v 0>"; diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index e3e259f7..6366906a 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -19,9 +19,9 @@ open Format open Camlcoq open Values open AST -open !Ctypes +open Ctypes open Cop -open !Csyntax +open Csyntax let name_unop = function | Onotbool -> "!" @@ -87,11 +87,11 @@ let rec name_cdecl id ty = match ty with | Tvoid -> "void" ^ name_optid id - | Tint(sz, sg, a) -> + | Ctypes.Tint(sz, sg, a) -> name_inttype sz sg ^ attributes a ^ name_optid id - | Tfloat(sz, a) -> + | Ctypes.Tfloat(sz, a) -> name_floattype sz ^ attributes a ^ name_optid id - | Tlong(sg, a) -> + | Ctypes.Tlong(sg, a) -> name_longtype sg ^ attributes a ^ name_optid id | Tpointer(t, a) -> let id' = @@ -182,7 +182,7 @@ let print_typed_value p v ty = fprintf p "%.15F" (camlfloat_of_coqfloat f) | Vsingle f, _ -> fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f) - | Vlong n, Tlong(Unsigned, _) -> + | Vlong n, Ctypes.Tlong(Unsigned, _) -> fprintf p "%LuLLU" (camlint64_of_coqint n) | Vlong n, _ -> fprintf p "%LdLL" (camlint64_of_coqint n) @@ -498,7 +498,7 @@ let print_globvar p id v = fprintf p "@[<hov 2>%s = " (name_cdecl name2 v.gvar_info); begin match v.gvar_info, v.gvar_init with - | (Tint _ | Tlong _ | Tfloat _ | Tpointer _ | Tfunction _), + | (Ctypes.Tint _ | Ctypes.Tlong _ | Ctypes.Tfloat _ | Tpointer _ | Tfunction _), [i1] -> print_init p i1 | _, il -> @@ -543,8 +543,8 @@ let print_program p prog = fprintf p "@[<v 0>"; List.iter (declare_composite p) prog.prog_types; List.iter (define_composite p) prog.prog_types; - List.iter (print_globdecl p) prog.prog_defs; - List.iter (print_globdef p) prog.prog_defs; + List.iter (print_globdecl p) prog.Ctypes.prog_defs; + List.iter (print_globdef p) prog.Ctypes.prog_defs; fprintf p "@]@." let destination : string option ref = ref None |