diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-08-21 10:18:56 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-08-21 10:18:56 +0200 |
| commit | 32c34a37e913b856e0267ad8c7ca6e65b96c0b23 (patch) | |
| tree | 92705f910dbb288e5b67a86bec40ecc14a039810 /cparser/Cutil.ml | |
| parent | a773dca6ddd1bca6b4780ea9387ab96deb001da8 (diff) | |
| download | compcert-kvx-32c34a37e913b856e0267ad8c7ca6e65b96c0b23.tar.gz compcert-kvx-32c34a37e913b856e0267ad8c7ca6e65b96c0b23.zip | |
Diagnostic for wrong application of restrict (#119)
Restrict is only allowed for pointers whose referenced type is an
object type or incomplete type, but not a function type.
Bug 23397
Diffstat (limited to 'cparser/Cutil.ml')
| -rw-r--r-- | cparser/Cutil.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index e25a1d84..1c9f747e 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -793,6 +793,11 @@ let is_anonymous_composite = function | TUnion (id,_) -> id.C.name = "" | _ -> false +let is_function_pointer_type env t = + match unroll env t with + | TPtr (ty, _) -> is_function_type env ty + | _ -> false + (* Find the info for a field access *) let field_of_dot_access env t m = |