aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2018-06-03 17:27:38 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-06-04 16:30:23 +0200
commit4a11a47faff0bad5f7f3d65b3c00569ba983414d (patch)
tree619a6bcbaade9e43dd621fe578ad049a2f2f81f4 /cparser/Elab.ml
parent08411be90dcce22cf92bca1c42331a8da884746e (diff)
downloadcompcert-kvx-4a11a47faff0bad5f7f3d65b3c00569ba983414d.tar.gz
compcert-kvx-4a11a47faff0bad5f7f3d65b3c00569ba983414d.zip
Warn that _Alignas and _Alignof are C11 extensions
Consistently with _Noreturn, anonymous structs, etc.
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 1d88e4ea..39b15279 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -517,6 +517,7 @@ let elab_attribute env = function
| PACKED_ATTR (args, loc) ->
[Attr("__packed__", List.map (elab_attr_arg loc env) args)]
| ALIGNAS_ATTR ([a], loc) ->
+ warning loc Celeven_extension "'_Alignas' is a C11 extension";
begin match elab_attr_arg loc env a with
| AInt n ->
if is_power_of_two n || n = 0L then
@@ -1783,8 +1784,9 @@ let elab_expr vararg loc env a =
| TYPE_ALIGNOF (spec, dcl) ->
let (ty, env') = elab_type loc env spec dcl in
+ warning Celeven_extension "'_Alignof' is a C11 extension";
if wrap incomplete_type loc env' ty then
- error "invalid application of 'alignof' to an incomplete type %a" (print_typ env) ty;
+ error "invalid application of '_Alignof' to an incomplete type %a" (print_typ env) ty;
{ edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) },env'
| BUILTIN_OFFSETOF ((spec,dcl), mem) ->