aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--cparser/Cutil.ml11
-rw-r--r--cparser/Cutil.mli2
-rw-r--r--cparser/Diagnostics.ml5
-rw-r--r--cparser/Diagnostics.mli1
-rw-r--r--cparser/Elab.ml16
5 files changed, 30 insertions, 5 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 3e2dff36..dcafbea4 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -1048,6 +1048,17 @@ let is_bitfield env e =
fld.fld_bitfield <> None
| _ -> false
+let contains_flex_array_mem env ty =
+ match unroll env ty with
+ | TStruct (id,_) ->
+ let ci = Env.find_struct env id in
+ let rec check_mem = function
+ | [] -> false
+ | [ { fld_typ = TArray(ty_elt, None, _) } ] -> true
+ | _::rem -> check_mem rem in
+ check_mem ci.ci_members
+ | _ -> false
+
(* Assignment compatibility check over attributes.
Standard attributes ("const", "volatile", "restrict") can safely
be added (to the rhs type to get the lhs type) but must not be dropped.
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 5ae5dcd7..9b09a413 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -250,6 +250,8 @@ val is_volatile_variable: Env.t -> exp -> bool
(* Test whether the expression is an access to a volatile variable *)
val is_bitfield: Env.t -> exp -> bool
(* Test whether the expression is a bit-field *)
+val contains_flex_array_mem : Env.t -> typ -> bool
+ (* Is this a struct with a flexible array member *)
(* Constructors *)
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index d0e35b72..52e5e456 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -95,6 +95,7 @@ type warning_type =
| Ignored_attributes
| Extern_after_definition
| Static_in_inline
+ | Flexible_array_extensions
(* List of active warnings *)
let active_warnings: warning_type list ref = ref [
@@ -153,6 +154,7 @@ let string_of_warning = function
| Ignored_attributes -> "ignored-attributes"
| Extern_after_definition -> "extern-after-definition"
| Static_in_inline -> "static-in-inline"
+ | Flexible_array_extensions -> "flexible-array-extensions"
(* Activate the given warning *)
let activate_warning w () =
@@ -203,6 +205,7 @@ let wall () =
Ignored_attributes;
Extern_after_definition;
Static_in_inline;
+ Flexible_array_extensions;
]
let wnothing () =
@@ -237,6 +240,7 @@ let werror () =
Ignored_attributes;
Extern_after_definition;
Static_in_inline;
+ Flexible_array_extensions;
]
(* Generate the warning key for the message *)
@@ -418,6 +422,7 @@ let warning_options =
error_option Ignored_attributes @
error_option Extern_after_definition @
error_option Static_in_inline @
+ error_option Flexible_array_extensions @
[Exact ("-Wfatal-errors"), Set error_fatal;
Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *)
Exact ("-fno-diagnostics-color"), Unset color_diagnostics;
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index 0d49cd0b..62c54314 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -52,6 +52,7 @@ type warning_type =
| Ignored_attributes (** attributes declarations after definition *)
| Extern_after_definition (** extern declaration after non-extern definition *)
| Static_in_inline (** static variable in non-static inline function *)
+ | Flexible_array_extensions (** usange of structs with flexible arrays in structs and arrays *)
val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a
(** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 9bce4da9..46861708 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -752,6 +752,8 @@ and elab_type_declarator ?(fundef = false) loc env ty = function
let a = add_attributes a (elab_cvspecs env cv_specs) in
if wrap incomplete_type loc env ty then
error loc "array type has incomplete element type %a" (print_typ env) ty;
+ if wrap contains_flex_array_mem loc env ty then
+ warning loc Flexible_array_extensions "%a may not be used as an array element due to flexible array member" (print_typ env) ty;
let sz' =
match sz with
| None ->
@@ -992,16 +994,20 @@ and elab_struct_or_union_info kind loc env members attrs =
duplicate acc rest in
duplicate [] m;
(* Check for incomplete types *)
- let rec check_incomplete = function
+ let rec check_incomplete only = function
| [] -> ()
- | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> ()
- (* C99: ty[] allowed as last field of a struct *)
+ | [ { fld_typ = TArray(ty_elt, None, _) ; fld_name = name } ] when kind = Struct ->
+ (* C99: ty[] allowed as last field of a struct, provided this is not the only field *)
+ if only then
+ error loc "flexible array member '%a' not allowed in otherwise empty struct" pp_field name;
| fld :: rem ->
if wrap incomplete_type loc env' fld.fld_typ then
(* Must be fatal otherwise we get problems constructing the init *)
fatal_error loc "member '%a' has incomplete type" pp_field fld.fld_name;
- check_incomplete rem in
- check_incomplete m;
+ if wrap contains_flex_array_mem loc env' fld.fld_typ && kind = Struct then
+ warning loc Flexible_array_extensions "%a may not be used as a struct member due to flexible array member" (print_typ env) fld.fld_typ;
+ check_incomplete false rem in
+ check_incomplete true m;
(* Warn for empty structs or unions *)
if m = [] then
if kind = Struct then begin