- Support for _Alignof(ty) operator from ISO C 2011

  and __alignof__(ty), __alignof__(expr) from GCC.
- Resurrected __builtin_memcpy_aligned, useful for files generated
  by Scade KCG 6.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

10 files changed, 27 insertions, 19 deletions

diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index c1b83cb..257f6c8 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -235,6 +235,7 @@ let transf_expr env ctx e =
     match e.edesc with
     | EConst _ -> e
     | ESizeof _ -> e
+    | EAlignof _ -> e
     | EVar _ -> e
 
     | EUnop(Odot s, e1) ->
diff --git a/cparser/C.mli b/cparser/C.mli
index 35e872d..52f02c4 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -151,6 +151,7 @@ type exp = { edesc: exp_desc; etyp: typ }
 and exp_desc =
   | EConst of constant
   | ESizeof of typ
+  | EAlignof of typ
   | EVar of ident
   | EUnop of unary_operator * exp
   | EBinop of binary_operator * exp * exp * typ
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index fbeb522..4fc01e5 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -246,6 +246,11 @@ let rec expr env e =
       | None -> raise Notconst
       | Some n -> I(Int64.of_int n)
       end
+  | EAlignof ty ->
+      begin match alignof env ty with
+      | None -> raise Notconst
+      | Some n -> I(Int64.of_int n)
+      end
   | EVar _ ->
       raise Notconst
   | EUnop(op, e1) ->
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index 17b2f98..54dfd67 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -58,6 +58,7 @@ let rec add_exp e =
   | EConst (CEnum(id, v)) -> addref id
   | EConst _ -> ()
   | ESizeof ty -> add_typ ty
+  | EAlignof ty -> add_typ ty
   | EVar id -> addref id
   | EUnop(op, e1) -> add_exp e1
   | EBinop(op, e1, e2, ty) -> add_exp e1; add_exp e2
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 5887e87..2924c3d 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -181,6 +181,7 @@ type associativity = LtoR | RtoL | NA
 let precedence = function               (* H&S section 7.2 *)
   | EConst _ -> (16, NA)
   | ESizeof _ -> (15, RtoL)
+  | EAlignof _ -> (15, RtoL)
   | EVar _ -> (16, NA)
   | EBinop(Oindex, _, _, _) -> (16, LtoR)
   | ECall _ -> (16, LtoR)
@@ -215,6 +216,7 @@ let rec exp pp (prec, a) =
   | EConst cst -> const pp cst
   | EVar id -> ident pp id
   | ESizeof ty -> fprintf pp "sizeof(%a)" typ ty
+  | EAlignof ty -> fprintf pp "__alignof(%a)" typ ty
   | EUnop(Ominus, a1) ->
       fprintf pp "-%a" exp (prec', a1)
   | EUnop(Oplus, a1) ->
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 2da1936..f9b70c4 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -867,6 +867,18 @@ let elab_expr loc env a =
         err "incomplete type %a" Cprint.typ ty;
       { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []) }
 
+  | EXPR_ALIGNOF a1 ->
+      let b1 = elab a1 in
+      if sizeof env b1.etyp = None then
+        err "incomplete type %a" Cprint.typ b1.etyp;
+      { edesc = EAlignof b1.etyp; etyp =  TInt(size_t_ikind, []) }
+
+  | TYPE_ALIGNOF (spec, dcl) ->
+      let ty = elab_type loc env spec dcl in
+      if sizeof env ty = None then
+        err "incomplete type %a" Cprint.typ ty;
+      { edesc = EAlignof ty; etyp =  TInt(size_t_ikind, []) }
+
   | UNARY(PLUS, a1) ->
       let b1 = elab a1 in
       if not (is_arith_type env b1.etyp) then
@@ -1110,25 +1122,6 @@ let elab_expr loc env a =
       error "GCC's &&label construct is not supported"
   | GNU_BODY _ ->
       error "GCC's statements within expressions are not supported"
-  | EXPR_ALIGNOF _ | TYPE_ALIGNOF _ ->
-      error "GCC's __alignof__ construct is not supported"
-
-(*
-  | EXPR_ALIGNOF a1 ->
-      warning "nonstandard `alignof' expression, turned into a constant";
-      let b1 = elab a1 in
-      begin match alignof env b1.etyp with
-      | None -> error "incomplete type %a" Cprint.typ b1.etyp
-      | Some al -> intconst (Int64.of_int al) size_t_ikind
-      end
-  | TYPE_ALIGNOF (spec, dcl) ->
-      warning "nonstandard `alignof' expression, turned into a constant";
-      let ty = elab_type loc env spec dcl in
-      begin match alignof env ty with
-      | None -> error "incomplete type %a" Cprint.typ ty
-      | Some al -> intconst (Int64.of_int al) size_t_ikind
-      end
-*)
 
 (* Elaboration of pre- or post- increment/decrement *)
   and elab_pre_post_incr_decr op msg a1 =
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index d4947ad..ab90bc2 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -145,6 +145,7 @@ let init_lexicon _ =
       ("__typeof__", fun loc -> TYPEOF loc);
       ("__typeof", fun loc -> TYPEOF loc);
       ("typeof", fun loc -> TYPEOF loc); 
+      ("_Alignof", fun loc -> ALIGNOF loc);
       ("__alignof", fun loc -> ALIGNOF loc);
       ("__alignof__", fun loc -> ALIGNOF loc);
       ("__volatile__", fun loc -> VOLATILE loc);
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 30466cb..ebdd86b 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -251,6 +251,7 @@ let transf_expr loc env ctx e =
     match e.edesc with
     | EConst _ -> e
     | ESizeof _ -> e
+    | EAlignof _ -> e
     | EVar _ -> e
 
     | EUnop(Odot _, _) | EUnop(Oarrow _, _) | EBinop(Oindex, _, _, _) ->
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index d58c8ad..0ce401f 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -102,6 +102,7 @@ let rec exp env e =
 and exp_desc env = function
   | EConst cst -> EConst(constant env cst)
   | ESizeof ty -> ESizeof(typ env ty)
+  | EAlignof ty -> EAlignof(typ env ty)
   | EVar id -> EVar(ident env id)
   | EUnop(op, a) -> EUnop(op, exp env a)
   | EBinop(op, a, b, ty) -> EBinop(op, exp env a, exp env b, typ env ty)
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 57246ce..dd985b1 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -57,6 +57,8 @@ let rec transf_expr env ctx e =
       {edesc = EConst c; etyp = newty}
   | ESizeof ty ->
       {edesc = ESizeof (transf_type env ty); etyp = newty}
+  | EAlignof ty ->
+      {edesc = EAlignof (transf_type env ty); etyp = newty}
   | EVar x ->
       {edesc = EVar x; etyp = newty}
   | EUnop(op, e1) ->