aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-08-22 13:01:50 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-08-22 13:01:50 +0200
commit2084c5b91929b9290b7e02979ee038bb98d1053e (patch)
tree4ce14e0abf19f83fcb03f60eee464c91169c3be2 /cparser
parentcc2d157be19d52bbe666e6d5a7ee9879cff7bfc8 (diff)
downloadcompcert-2084c5b91929b9290b7e02979ee038bb98d1053e.tar.gz
compcert-2084c5b91929b9290b7e02979ee038bb98d1053e.zip
Test for incomplete type during initialization.
Before the initializazion is computed we check wether the type is incomplete. Bug 19601
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Elab.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index b2426738..99370df6 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1287,7 +1287,12 @@ and elab_single zi a il =
(* Start with top-level object initialized to default *)
-in elab_item (I.top env root ty_root) ie []
+in
+if wrap incomplete_type loc env ty_root then begin
+ error loc "variable has incomplete type %a" Cprint.typ ty_root;
+ raise Exit
+end;
+elab_item (I.top env root ty_root) ie []
(* Elaboration of a top-level initializer *)