From 83d60a2059f171509b5e7bb14ac70846488ebd8e Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 18 Feb 2012 09:04:24 +0000 Subject: Don't print external declarations for builtins. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1818 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/PrintClight.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'cfrontend/PrintClight.ml') diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 83a0747..77f22f7 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -245,9 +245,11 @@ let print_function p id f = let print_fundef p (id, fd) = match fd with - | External(_, args, res) -> + | External(EF_external(_,_), args, res) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res))) + | External(_, _, _) -> + () | Internal f -> print_function p id f @@ -326,7 +328,7 @@ let print_struct_or_union p (name, fld) = fprintf p "@ %s;" (name_cdecl (extern_atom id) ty); print_fields rem in print_fields fld; - fprintf p "@;<0 -2>};@]@ " + fprintf p "@;<0 -2>};@]@ @ " let print_program p prog = struct_unions := StructUnionSet.empty; -- cgit v1.2.3