From 53b57751c1981e0bce3aa470e426a12034bb165e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 17 Sep 2006 08:58:05 +0000
Subject: Ajout de Init_pointer (experimental)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/PrintCsyntax.ml | 32 ++++++++++++++++++++++++++++++++
 caml/PrintPPC.ml     | 23 +++++++++++++++++++++--
 2 files changed, 53 insertions(+), 2 deletions(-)

(limited to 'caml')

diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml
index 6e88da98..052581cd 100644
--- a/caml/PrintCsyntax.ml
+++ b/caml/PrintCsyntax.ml
@@ -309,6 +309,34 @@ let print_fundef p (Coq_pair(id, fd)) =
   | Internal f ->
       print_function p id f
 
+let string_of_init id =
+  try
+    let s = String.create (length_coqlist id) in
+    let i = ref 0 in
+    coqlist_iter
+      (function
+        | Init_int8 n ->
+            s.[!i] <- Char.chr(Int32.to_int(camlint_of_coqint n));
+            incr i
+        | _ -> raise Not_found)
+      id;
+    Some s
+  with Not_found -> None
+
+let print_escaped_string p s =
+  fprintf p "\"";
+  for i = 0 to String.length s - 1 do
+    match s.[i] with
+    | ('\"' | '\\') as c -> fprintf p "\\%c" c
+    | '\n' -> fprintf p "\\n"
+    | '\t' -> fprintf p "\\t"
+    | '\r' -> fprintf p "\\r"
+    | c    -> if c >= ' ' && c <= '~'
+              then fprintf p "%c" c
+              else fprintf p "\\x%02x" (Char.code c)
+  done;
+  fprintf p "\""
+
 let print_init p = function
   | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n)
   | Init_int16 n -> fprintf p "%ld,@ " (camlint_of_coqint n)
@@ -316,6 +344,10 @@ let print_init p = function
   | Init_float32 n -> fprintf p "%F,@ " n
   | Init_float64 n -> fprintf p "%F,@ " n
   | Init_space n -> fprintf p "/* skip %ld*/@ " (camlint_of_coqint n)
+  | Init_pointer id ->
+      match string_of_init id with
+      | None -> fprintf p "/* pointer to other init*/,@ "
+      | Some s -> fprintf p "%a,@ " print_escaped_string s
 
 let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
   match init with
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;
-- 
cgit