diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-08-20 11:16:42 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-08-20 11:16:42 +0200 |
commit | 778d0cc5f87472f2da267be8356e5aef7fb75f96 (patch) | |
tree | f73e4af31380008c555512497a12ac9ec67398e8 /cparser | |
parent | 939977c7142222d0ec0b67322b06daa187a7b829 (diff) | |
download | compcert-778d0cc5f87472f2da267be8356e5aef7fb75f96.tar.gz compcert-778d0cc5f87472f2da267be8356e5aef7fb75f96.zip |
Improve support and diagnostic for type qualified arrays (#118)
* Add diagnostic for type qualified arrays that occur in the wrong place
Arrays with type qualifiers (e.g. int t[const 5]) are only allowed as
function parameters and for them
only the outermost array type derivation.
Bug 23400
* Keep attributes from array for argument conversion
Type qualifiers of arrays in function parameters are just syntactic sugar
to allow adding them to the resulting pointer type. Hence, when a
qualified array type such as `int t[const 5]` decays into a pointer type
during argument conversion, the pointer type should be qualified, e.g. `int * const t`.
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Cutil.ml | 11 | ||||
-rw-r--r-- | cparser/Cutil.mli | 2 | ||||
-rw-r--r-- | cparser/Elab.ml | 6 |
3 files changed, 18 insertions, 1 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index dcafbea4..e25a1d84 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -824,6 +824,15 @@ let float_rank = function | FDouble -> 2 | FLongDouble -> 3 +(* Test for qualified array types *) + +let rec is_qualified_array = function + | TArray (ty, _, attr) -> + List.exists attr_is_standard attr || is_qualified_array ty + | TPtr (ty, _) -> is_qualified_array ty + | TFun(ty_ret, _, _, _) -> is_qualified_array ty_ret + | _ -> false + (* Array and function types "decay" to pointer types in many cases *) let pointer_decay env t = @@ -901,7 +910,7 @@ let argument_conversion env t = (* Arrays and functions degrade automatically to pointers *) (* Other types are not changed *) match unroll env t with - | TArray(ty, _, _) -> TPtr(ty, []) + | TArray(ty, _, attr) -> TPtr(ty, attr) | TFun _ as ty -> TPtr(ty, []) | _ -> t (* preserve typedefs *) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 9b09a413..43cbe9bd 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -175,6 +175,8 @@ val integer_rank : ikind -> int (* Order integer kinds from smaller to bigger *) val float_rank : fkind -> int (* Order float kinds from smaller to bigger *) +val is_qualified_array : typ -> bool + (* Does the type contain a qualified array type (e.g. int[const 5])? *) (* Usual conversions over types *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index cc7648e0..da5a1d37 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -835,6 +835,8 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = error loc "redefinition of parameter '%s'" id; (* replace array and function types by pointer types *) let ty1 = argument_conversion env1 ty in + if is_qualified_array ty1 then + error loc "type qualifier used in non-outermost array type derivation"; let (id', env2) = Env.enter_ident env1 id sto ty1 in ( (id', ty1) , env2) @@ -953,6 +955,8 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = error loc "bit-field '%a' width not an integer constant" pp_field id; None,env end in + if is_qualified_array ty then + error loc "type qualifier used in array declarator outside of function prototype"; let anon_composite = is_anonymous_composite ty in if id = "" && not anon_composite && optbitsize = None then warning loc Missing_declarations "declaration does not declare anything"; @@ -2334,6 +2338,8 @@ let enter_decdefs local nonstatic_inline loc env sto dl = (name_of_storage_class sto) | _ -> () end; + if is_qualified_array ty then + error loc "type qualifier used in array declarator outside of function prototype"; (* Local variable declarations with default storage are treated as 'auto'. Local function declarations with default storage remain with default storage. *) |