From 97ef3561168a6262833e65aba379ab9aca1a1a17 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 22 Aug 2016 15:46:40 +0200
Subject: Also print declarations in CompCert C.

The PrintCsyntax now first emits declarations for all functions
and variables in order to allow foward declarations.
Bug 19598.
---
 cfrontend/PrintCsyntax.ml | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'cfrontend/PrintCsyntax.ml')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index a15fb0e4..7b2fc108 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -434,6 +434,14 @@ let print_fundef p id fd =
   | Ctypes.Internal f ->
       print_function p id f
 
+let print_fundecl p id fd =
+  match fd with
+  | Ctypes.Internal f ->
+      let linkage = if C2C.atom_is_static id then "static" else "extern" in
+      fprintf p "%s %s;@ @ " linkage
+                (name_cdecl (extern_atom id) (Csyntax.type_of_function f))
+  | _ -> ()
+
 let string_of_init id =
   let b = Buffer.create (List.length id) in
   let add_init = function
@@ -501,6 +509,17 @@ let print_globvar p id v =
       end;
       fprintf p ";@]@ @ "
 
+let print_globvardecl p  id v =
+  let name = extern_atom id in
+  let name = if v.gvar_readonly then "const "^name else name in
+  let linkage = if C2C.atom_is_static id then "static" else "extern" in
+  fprintf p "%s %s;@ @ " linkage (name_cdecl name v.gvar_info)
+
+let print_globdecl p (id,gd) =
+  match gd with
+  | Gfun f -> print_fundecl p id f
+  | Gvar v -> print_globvardecl p id v
+
 let print_globdef p (id, gd) =
   match gd with
   | Gfun f -> print_fundef p id f
@@ -524,6 +543,7 @@ let print_program p prog =
   fprintf p "@[<v 0>";
   List.iter (declare_composite p) prog.prog_types;
   List.iter (define_composite p) prog.prog_types;
+  List.iter (print_globdecl p) prog.prog_defs;
   List.iter (print_globdef p) prog.prog_defs;
   fprintf p "@]@."
 
-- 
cgit