From 033aa0555a209fa3e825b1eeb8a5fc00ff8163e3 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 1 Nov 2009 09:55:35 +0000
Subject: Support Clight initializers of the form "int * x = &y;".

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/PrintCsyntax.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'cfrontend/PrintCsyntax.ml')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 88e24eed..fa1d0482 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -378,6 +378,11 @@ 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_addrof(symb, ofs) ->
+      let ofs = camlint_of_coqint ofs in
+      if ofs = 0l
+      then fprintf p "&%s,@ " (extern_atom symb)
+      else fprintf p "(void *)((char *)&%s + %ld),@ " (extern_atom symb) ofs
   | Init_pointer id ->
       match string_of_init id with
       | None -> fprintf p "/* pointer to other init*/,@ "
-- 
cgit