diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-18 09:04:24 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-18 09:04:24 +0000 |
commit | 83d60a2059f171509b5e7bb14ac70846488ebd8e (patch) | |
tree | fc583126495167fabf41e56f139e9493dc0d28de /cfrontend | |
parent | 14b44ae202de640f2a7a6e973e5fb912b736c002 (diff) |
Don't print external declarations for builtins.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1818 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/PrintClight.ml | 6 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 6 |
2 files changed, 8 insertions, 4 deletions
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; diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index d4e728e..804b018 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -345,9 +345,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 @@ -505,7 +507,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; |