diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-08-20 10:42:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-08-20 10:42:21 +0200 |
| commit | e9b5632617b1477603883aab543994e2a1c464ce (patch) | |
| tree | d2f67322c1ff09ed2a6c6c3aa64e8b40421ade33 /cparser/Elab.ml | |
| parent | 6fc89e5c8c4a8f98ef0a4a03c00994bbfb146431 (diff) | |
| download | compcert-kvx-e9b5632617b1477603883aab543994e2a1c464ce.tar.gz compcert-kvx-e9b5632617b1477603883aab543994e2a1c464ce.zip | |
Additional checks for flex arrays in structs (#93)
* Error for structs with only flex array member
Flexible array members are only allowed if another member exists.
Bug 23324
* Added checks for nesting of structs with flex array members
Warn if a struct with a flex array member is used as array element
or member of another struct. Such usage is dubious.
Bug 23324
Don't warn if the struct-with-flex-array is a member of an union.
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 16 |
1 files changed, 11 insertions, 5 deletions
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 |