aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-04-22 10:09:05 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-04-22 11:09:05 +0300
commit1106670d8b48ec4883f66b5c43f9e8e7757006e5 (patch)
tree9be39ce8e2b082bece43cd16651e452f607e9fba
parent90f83fd516f625f21533c7c8d775bf630bbacdb5 (diff)
downloadcompcert-1106670d8b48ec4883f66b5c43f9e8e7757006e5.tar.gz
compcert-1106670d8b48ec4883f66b5c43f9e8e7757006e5.zip
Accept empty enum declaration after nonempty enum definition (#87)
Forward declarations of enums are not allowed in C99, however it is possible to have an empty enum declaration after the enum was defined.
-rw-r--r--cparser/Elab.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index f203c777..d5e30d9f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -996,7 +996,7 @@ and elab_enum only loc tag optmembers attrs env =
let tag = match tag with None -> "" | Some s -> s in
match optmembers with
| None ->
- if only then
+ if only && not (redef Env.lookup_enum env tag) then
fatal_error loc
"forward declaration of 'enum %s' is not allowed in ISO C" tag;
let (tag', info) = wrap Env.lookup_enum loc env tag in (tag', env)