aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2018-08-17 15:42:23 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-08-24 09:26:50 +0200
commitb6542ff823fb431b6f22724da5ab5cbbdfe01598 (patch)
tree04db74994fa2bebb6cc0e9409a896503564e6f81
parentb5b368a37478de36929da9e1fa694f989d124764 (diff)
downloadcompcert-kvx-b6542ff823fb431b6f22724da5ab5cbbdfe01598.tar.gz
compcert-kvx-b6542ff823fb431b6f22724da5ab5cbbdfe01598.zip
Preserve attribute(("aligned")) in the AST, don't map it to _Alignas
We used to recognize attribute(("aligned"(N))) and map it to _Alignas(N) during elaboration. However, we want to restrict the places where _Alignas can occur, as standardized in ISO C11, while leaving more freedom for the placement of the "aligned" attribute. As a first step in this direction, this commit keeps the "aligned" attribute unchanged in the AST, and distinct from _Alignas attributes. Both attributes are honored when it comes to determining the actual alignment of a type.
-rw-r--r--cparser/Cutil.ml2
-rw-r--r--cparser/Elab.ml3
2 files changed, 3 insertions, 2 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 1c9f747e..8b6d5e32 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -264,6 +264,8 @@ let alignas_attribute al =
let rec alignas_attr accu = function
| [] -> accu
| AAlignas n :: al -> alignas_attr (max n accu) al
+ | Attr(("aligned" | "__aligned__"), [AInt n]) :: al ->
+ alignas_attr (max (Int64.to_int n) accu) al
| a :: al -> alignas_attr accu al
in alignas_attr 0 al
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 257bc621..1f2c588f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -511,8 +511,7 @@ let enter_gcc_attr loc a =
match a with
| Attr(("aligned"|"__aligned__"), args) ->
begin match args with
- | [AInt n] ->
- if check_alignment loc n then [AAlignas (Int64.to_int n)] else []
+ | [AInt n] -> if check_alignment loc n then [a] else []
| [_] -> error loc "requested alignment is not an integer constant"; []
| [] -> [] (* Use default alignment, like gcc does *)
| _ -> error loc "'aligned' attribute takes no more than 1 argument"; []