diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-17 08:58:05 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-17 08:58:05 +0000 |
commit | 53b57751c1981e0bce3aa470e426a12034bb165e (patch) | |
tree | 8f33000862413e7a687475fad228515d5b74527c /caml/PrintPPC.ml | |
parent | 3f1fb601a23c63eb5c619330c632b6f2dba36ad7 (diff) | |
download | compcert-53b57751c1981e0bce3aa470e426a12034bb165e.tar.gz compcert-53b57751c1981e0bce3aa470e426a12034bb165e.zip |
Ajout de Init_pointer (experimental)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/PrintPPC.ml')
-rw-r--r-- | caml/PrintPPC.ml | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index b7db5014..85d695e1 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -382,7 +382,9 @@ let print_fundef oc (Coq_pair(name, defn)) = | Internal code -> print_function oc name code | External ef -> print_external_function oc name -let print_init_data oc = function +let init_data_queue = ref [] + +let print_init oc = function | Init_int8 n -> fprintf oc " .byte %ld\n" (camlint_of_coqint n) | Init_int16 n -> @@ -401,6 +403,23 @@ let print_init_data oc = function | Init_space n -> let n = camlint_of_z n in if n > 0l then fprintf oc " .space %ld\n" n + | Init_pointer id -> + let lbl = new_label() in + fprintf oc " .long L%d\n" lbl; + init_data_queue := (lbl, id) :: !init_data_queue + +let print_init_data oc id = + init_data_queue := []; + coqlist_iter (print_init oc) id; + let rec print_remainder () = + match !init_data_queue with + | [] -> () + | (lbl, id) :: rem -> + init_data_queue := rem; + fprintf oc "L%d:\n" lbl; + coqlist_iter (print_init oc) id; + print_remainder() + in print_remainder() let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = match init_data with @@ -409,7 +428,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = fprintf oc " .data\n"; fprintf oc " .globl %a\n" print_symb name; fprintf oc "%a:\n" print_symb name; - coqlist_iter (print_init_data oc) init_data + print_init_data oc init_data let print_program oc p = extfuns := IdentSet.empty; |