aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-08-23 10:50:48 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-08-23 10:50:48 +0200
commitc3c0aba2ed285bc33208cfc67667f47d6d1b0762 (patch)
tree666ace2761c58fde7fabd3668dda1d29540def5e /cparser
parente829671ab99a98dca212c6f29d29b952dbc1fa80 (diff)
downloadcompcert-kvx-c3c0aba2ed285bc33208cfc67667f47d6d1b0762.tar.gz
compcert-kvx-c3c0aba2ed285bc33208cfc67667f47d6d1b0762.zip
Fix for initialization of incomplete types
Since some incomplete types are allowed in initialization just test whether the default initilization exists. Bug 19601
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Cutil.ml5
-rw-r--r--cparser/Cutil.mli2
-rw-r--r--cparser/Elab.ml6
3 files changed, 8 insertions, 5 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 4b4e1b81..c8966941 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -1026,6 +1026,7 @@ let formatloc pp (filename, lineno) =
if filename <> "" then Format.fprintf pp "%s:%d: " filename lineno
(* Generate the default initializer for the given type *)
+exception No_default_init
let rec default_init env ty =
match unroll env ty with
@@ -1049,11 +1050,11 @@ let rec default_init env ty =
| TUnion(id, _) ->
let ci = Env.find_union env id in
begin match ci.ci_members with
- | [] -> assert false
+ | [] -> raise No_default_init
| fld :: _ -> Init_union(id, fld, default_init env fld.fld_typ)
end
| _ ->
- assert false
+ raise No_default_init
(* Substitution of variables by expressions *)
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 91b073ab..8d461e5c 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -244,6 +244,8 @@ val formatloc: Format.formatter -> location -> unit
(* Printer for locations (for Format) *)
(* Initializers *)
+exception No_default_init
+ (* Raised if no default initilaizer exists *)
val default_init: Env.t -> typ -> init
(* Return a default initializer for the given type
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 16e2b298..f8d2cb77 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1292,11 +1292,11 @@ if is_function_type env ty_root then begin
error loc "illegal initializer (only variables can be initialized)";
raise Exit
end;
-if wrap incomplete_type loc env ty_root then begin
+try
+ elab_item (I.top env root ty_root) ie []
+with No_default_init ->
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 *)