From ce4951549999f403446415c135ad1403a16a15c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Nov 2012 13:42:22 +0000 Subject: Globalenvs: allocate one-byte block with permissions Nonempty for each function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/PrintAsm.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'ia32/PrintAsm.ml') diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index a36adb1..08bd2f5 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -767,11 +767,6 @@ let print_function oc name code = jumptables := [] end -let print_fundef oc (name, defn) = - match defn with - | Internal code -> print_function oc name code - | External ef -> () - let print_init oc = function | Init_int8 n -> fprintf oc " .byte %ld\n" (camlint_of_coqint n) @@ -802,7 +797,7 @@ let print_init_data oc name id = else List.iter (print_init oc) id -let print_var oc (name, v) = +let print_var oc name v = match v.gvar_init with | [] -> () | _ -> @@ -826,11 +821,16 @@ let print_var oc (name, v) = fprintf oc " .size %a, . - %a\n" symbol name symbol name end +let print_globdef oc (name, gdef) = + match gdef with + | Gfun(Internal code) -> print_function oc name code + | Gfun(External ef) -> () + | Gvar v -> print_var oc name v + let print_program oc p = need_masks := false; indirect_symbols := StringSet.empty; - List.iter (print_var oc) p.prog_vars; - List.iter (print_fundef oc) p.prog_funct; + List.iter (print_globdef oc) p.prog_defs; if !need_masks then begin section oc Section_const; (* not Section_literal because not 8-bytes *) print_align oc 16; -- cgit v1.2.3