diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-22 15:46:40 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-22 15:46:40 +0200 |
commit | 97ef3561168a6262833e65aba379ab9aca1a1a17 (patch) | |
tree | 1ea46137d9c9ecc4269bd6bde494436898b6a6a0 | |
parent | 0200f6b77550e95c0ec309d1a44f5253fc790e4f (diff) | |
download | compcert-97ef3561168a6262833e65aba379ab9aca1a1a17.tar.gz compcert-97ef3561168a6262833e65aba379ab9aca1a1a17.zip |
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.
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 20 |
1 files changed, 20 insertions, 0 deletions
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 "@]@." |