diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
| commit | ce4951549999f403446415c135ad1403a16a15c3 (patch) | |
| tree | cac9bbb2fea29fce331916b277c38ed8fe29e471 /backend/PrintCminor.ml | |
| parent | dcb9f48f51cec5e864565862a700c27df2a1a7e6 (diff) | |
| download | compcert-kvx-ce4951549999f403446415c135ad1403a16a15c3.tar.gz compcert-kvx-ce4951549999f403446415c135ad1403a16a15c3.zip | |
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
Diffstat (limited to 'backend/PrintCminor.ml')
| -rw-r--r-- | backend/PrintCminor.ml | 23 |
1 files changed, 10 insertions, 13 deletions
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 858ef219..8e49303d 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -273,13 +273,6 @@ let print_extfun p id ef = fprintf p "@[<v 0>extern @[<hov 2>\"%s\":@ %a@]@ " (extern_atom id) print_sig (ef_sig ef) -let print_fundef p (id, fd) = - match fd with - | External ef -> - print_extfun p id ef - | Internal f -> - print_function p id f - let print_init_data p = function | Init_int8 i -> fprintf p "int8 %ld" (camlint_of_coqint i) | Init_int16 i -> fprintf p "int16 %ld" (camlint_of_coqint i) @@ -306,14 +299,18 @@ let print_globvar p gv = print_init_data_list p gv.gvar_init; fprintf p "}" -let print_var p (id, gv) = - fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv +let print_globdef p (id, gd) = + match gd with + | Gfun(External ef) -> + print_extfun p id ef + | Gfun(Internal f) -> + print_function p id f + | Gvar gv -> + fprintf p "var \"%s\" %a\n" (extern_atom id) print_globvar gv let print_program p prog = - fprintf p "@[<v>"; - List.iter (print_var p) prog.prog_vars; - fprintf p "@]@[<v 0>"; - List.iter (print_fundef p) prog.prog_funct; + fprintf p "@[<v 0>"; + List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." let destination : string option ref = ref None |