From aa5ddeddbe50487f6671b80d1a58a09d619d6f66 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 22 Aug 2016 10:04:53 +0200
Subject: Added missing , in PrintCsyntax. Bug 19599

---
 cfrontend/PrintCsyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'cfrontend/PrintCsyntax.ml')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 7933f987..a15fb0e4 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -401,7 +401,7 @@ let name_function_parameters fun_name params cconv =
   | _ ->
       let rec add_params first = function
       | [] ->
-          if cconv.cc_vararg then Buffer.add_string b "..."
+          if cconv.cc_vararg then Buffer.add_string b ",..."
       | (id, ty) :: rem ->
           if not first then Buffer.add_string b ", ";
           Buffer.add_string b (name_cdecl (extern_atom id) ty);
-- 
cgit 


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 


From b55d63d2917b384fa0f5da76d7d16036ad263847 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 23 Aug 2016 12:32:50 +0200
Subject: Print prototypes for malloc and free.

The declarations of malloc and free should also be printed for
CompCert C.
Bug 19616.
---
 cfrontend/PrintCsyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'cfrontend/PrintCsyntax.ml')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 7b2fc108..e3e259f7 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -426,7 +426,7 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) ->
+  | Ctypes.External((EF_external _ | EF_runtime _| EF_malloc | EF_free), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
                 (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
   | Ctypes.External(_, _, _, _) ->
-- 
cgit