diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-08 15:44:11 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-08 15:44:11 +0000 |
commit | b068e4229062a84548c1ae20487b273ea6bb37db (patch) | |
tree | c058e373adbee2129f7cff531c57a20488c1da5e /caml/PrintCsyntax.ml | |
parent | a5b33dcab2e6218e9e17f36a26520fd1dabc58bb (diff) |
Suite de l'adaptation du front-end CIL
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@87 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/PrintCsyntax.ml')
-rw-r--r-- | caml/PrintCsyntax.ml | 52 |
1 files changed, 30 insertions, 22 deletions
diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml index ff2af16..da257bd 100644 --- a/caml/PrintCsyntax.ml +++ b/caml/PrintCsyntax.ml @@ -93,13 +93,18 @@ let rec name_cdecl id ty = then Buffer.add_string b "(*)" else Buffer.add_string b (parenthesize_if_pointer id); Buffer.add_char b '('; - let rec add_args first = function - | Tnil -> () - | Tcons(t1, tl) -> - if not first then Buffer.add_string b ", "; - Buffer.add_string b (name_cdecl "" t1); - add_args false tl in - add_args true args; + begin match args with + | Tnil -> + Buffer.add_string b "void" + | _ -> + let rec add_args first = function + | Tnil -> () + | Tcons(t1, tl) -> + if not first then Buffer.add_string b ", "; + Buffer.add_string b (name_cdecl "" t1); + add_args false tl in + add_args true args + end; Buffer.add_char b ')'; name_cdecl (Buffer.contents b) res | Tstruct fld -> @@ -274,13 +279,18 @@ let name_function_parameters fun_name params = let b = Buffer.create 20 in Buffer.add_string b fun_name; Buffer.add_char b '('; - let rec add_params first = function - | Coq_nil -> () - | Coq_cons(Coq_pair(id, ty), rem) -> - if not first then Buffer.add_string b ", "; - Buffer.add_string b (name_cdecl (extern_atom id) ty); - add_params false rem in - add_params true params; + begin match params with + | Coq_nil -> + Buffer.add_string b "void" + | _ -> + let rec add_params first = function + | Coq_nil -> () + | Coq_cons(Coq_pair(id, ty), rem) -> + if not first then Buffer.add_string b ", "; + Buffer.add_string b (name_cdecl (extern_atom id) ty); + add_params false rem in + add_params true params + end; Buffer.add_char b ')'; Buffer.contents b @@ -300,7 +310,7 @@ let print_function p id f = let print_fundef p (Coq_pair(id, fd)) = match fd with | External(_, args, res) -> - fprintf p "extern %s;@ " + fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res))) | Internal f -> print_function p id f @@ -316,16 +326,16 @@ let print_init p = function let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = match init with | Coq_nil -> - fprintf p "extern %s;@ " + fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) ty) | Coq_cons(Init_space _, Coq_nil) -> - fprintf p "%s;@ " + fprintf p "%s;@ @ " (name_cdecl (extern_atom id) ty) | _ -> fprintf p "@[<hov 2>%s = {@ " (name_cdecl (extern_atom id) ty); coqlist_iter (print_init p) init; - fprintf p "};@]@ " + fprintf p "};@]@ @ " (* Collect struct and union types *) @@ -408,13 +418,13 @@ let collect_program p = coqlist_iter collect_fundef p.prog_funct let print_struct_or_union p ((kind, fld), name) = - fprintf p "@[<v 2>%s %s{@ " + fprintf p "@[<v 2>%s %s {" (match kind with Struct -> "struct" | Union -> "union") name; let rec print_fields = function | Fnil -> () | Fcons(id, ty, rem) -> - fprintf p "%s; @ " (name_cdecl (extern_atom id) ty); + fprintf p "@ %s;" (name_cdecl (extern_atom id) ty); print_fields rem in print_fields fld; fprintf p "@;<0 -2>}@]@ " @@ -425,9 +435,7 @@ let print_program p prog = collect_program prog; fprintf p "@[<v 0>"; List.iter (print_struct_or_union p) !struct_union_names; - fprintf p "@ "; coqlist_iter (print_globvar p) prog.prog_vars; - fprintf p "@ "; coqlist_iter (print_fundef p) prog.prog_funct; fprintf p "@]@." |