summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-13 15:58:10 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-13 15:58:10 +0000
commit16ef95d7d7df64e28f6ba4ad24457b946563bc2e (patch)
tree2f204e78ef82df3269c0b2ba2b86d279946d9922
parenta558eac3b8c9929a4c29236baada4c4b4360b6ff (diff)
Spurious error on a local static function declaration
("static int f(void);" inside a function). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2563 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--cparser/Elab.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 24a3709..f6ee199 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1779,6 +1779,7 @@ let enter_decdefs local loc env sto dl =
let env2 = Env.add_ident env1 id sto' ty' in
(* check for incomplete type *)
if local && sto' <> Storage_extern
+ && not (is_function_type env ty')
&& wrap incomplete_type loc env ty' then
error loc "'%s' has incomplete type" s;
if local && sto' <> Storage_extern && sto' <> Storage_static then