aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-09-22 08:48:16 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-09-22 08:48:16 +0200
commit01a154119c41accf35e41f34f761170687fe2979 (patch)
treeba2309d76eb6a19c9b8800bfd478db917eabded1 /cparser
parentccb110fc5532796e63553150a0b0ef91a0bccd61 (diff)
downloadcompcert-01a154119c41accf35e41f34f761170687fe2979.tar.gz
compcert-01a154119c41accf35e41f34f761170687fe2979.zip
Reverted noisy change.
In order to empty declarations it is necessary to distinguish between forward declarations and empty declarations. Bug 19859
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Elab.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 9cdf6c29..b6418217 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2019,7 +2019,7 @@ let enter_decdefs local loc env sto dl =
(* Sanity checks on storage class *)
if sto = Storage_register && not local then
fatal_error loc "'register' storage-class on file-scoped variable";
- if dl = [] then
+ if sto <> Storage_default && dl = [] then
warning loc Missing_declarations "declaration does not declare anything";
let enter_decdef (decls, env) (s, ty, init) =
let isfun = is_function_type env ty in