Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-if-conversion

7 files changed, 229 insertions, 208 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index cf67015a..7329767a 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -947,7 +947,7 @@ let binary_conversion env t1 t2 =
       end
   | _, _ -> assert false
 
-(* Conversion on function arguments (with protoypes) *)
+(* Conversion on function arguments (with prototypes) *)
 
 let argument_conversion env t =
   (* Arrays and functions degrade automatically to pointers *)
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index 172affab..51dcab47 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -18,6 +18,10 @@
 open Format
 open Commandline
 
+(* Ensure that the error formatter is flushed at exit *)
+let _ =
+  at_exit (pp_print_flush err_formatter)
+
 (* Should errors be treated as fatal *)
 let error_fatal = ref false
 
@@ -28,7 +32,7 @@ let max_error = ref 0
 let diagnostics_show_option = ref true
 
 (* Test if color diagnostics are available by testing if stderr is a tty
-   and if the environment varibale TERM is set
+   and if the environment variable TERM is set
 *)
 let color_diagnostics =
   let term = try Sys.getenv "TERM" with Not_found -> "" in
@@ -469,7 +473,7 @@ let raise_on_errors () =
 let crash exn =
   if Version.buildnr <> "" && Version.tag <> "" then begin
     let backtrace = Printexc.get_backtrace () in
-    eprintf "%tThis is CompCert, %s, Build:%s, Tag:%s%t\n"
+    eprintf "%tThis is CompCert, Release %s, Build:%s, Tag:%s%t\n"
       bc Version.version Version.buildnr Version.tag rsc;
     eprintf "Backtrace (please include this in your support request):\n%s"
       backtrace;
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index ded8019f..6a3c11c8 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -22,22 +22,22 @@ exception Abort
   (** Exception raised upon fatal errors *)
 
 val check_errors : unit -> unit
-  (** Check whether errors occured and raise abort if an error occured *)
+  (** Check whether errors occurred and raise abort if an error occurred *)
 
 type warning_type =
   | Unnamed                        (** warnings which cannot be turned off *)
   | Unknown_attribute              (** usage of unsupported/unknown attributes *)
-  | Zero_length_array              (** gnu extension for zero lenght arrays *)
+  | Zero_length_array              (** gnu extension for zero length arrays *)
   | Celeven_extension              (** C11 features *)
   | Gnu_empty_struct               (** gnu extension for empty struct *)
-  | Missing_declarations           (** declation which do not declare anything *)
+  | Missing_declarations           (** declaration which do not declare anything *)
   | Constant_conversion            (** dangerous constant conversions *)
   | Int_conversion                 (** pointer <-> int conversions *)
   | Varargs                        (** promotable vararg argument *)
   | Implicit_function_declaration  (** deprecated implicit function declaration *)
   | Pointer_type_mismatch          (** pointer type mismatch in ?: operator *)
   | Compare_distinct_pointer_types (** comparison between different pointer types *)
-  | Implicit_int                   (** implict int parameter or return type *)
+  | Implicit_int                   (** implicit int parameter or return type *)
   | Main_return_type               (** wrong return type for main *)
   | Invalid_noreturn               (** noreturn function containing return *)
   | Return_type                    (** void return in non-void function *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 7a0b05de..9cca930d 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -295,14 +295,16 @@ let parse_int base s =
     |  _ -> assert false in
   let v = ref 0L in
   for i = 0 to String.length s - 1 do
-    if !v < 0L || !v > max_val then raise Overflow;
-    v := Int64.mul !v (Int64.of_int base);
     let c = s.[i] in
     let digit =
       if c >= '0' && c <= '9' then Char.code c - 48
       else if c >= 'A' && c <= 'F' then Char.code c - 55
       else raise Bad_digit in
     if digit >= base then raise Bad_digit;
+    if !v < 0L || !v > max_val then raise Overflow;
+    (* because (2^64 - 1) % 10 = 5, not 9 *)
+    if base = 10 && !v = max_val && digit > 5 then raise Overflow;
+    v := Int64.mul !v (Int64.of_int base);
     v := Int64.add !v (Int64.of_int digit)
   done;
   !v
@@ -939,31 +941,7 @@ and elab_name_group loc env  (spec, namelist) =
     ((id, add_attributes_type a ty), env1) in
   (mmap elab_one_name env' namelist, sto)
 
-(* Elaboration of an init-name group *)
 
-and elab_init_name_group loc env (spec, namelist) =
-  let (sto, inl, noret, tydef, bty, env') =
-    elab_specifier ~only:(namelist=[]) loc env spec in
-  if noret && tydef then
-    error loc "'_Noreturn' can only appear on functions";
-  let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) =
-    let ((ty, _), env1) =
-      elab_type_declarator loc env bty decl in
-    let a = elab_attributes env attr in
-    let has_fun_typ = is_function_type env ty in
-    if inl && not has_fun_typ then
-      error loc "'inline' can only appear on functions";
-    let a' =
-      if noret then begin
-        warning loc Celeven_extension "_Noreturn functions are a C11 extension";
-        if not has_fun_typ then
-          error loc "'_Noreturn' can only appear on functions";
-        add_attributes [Attr("noreturn",[])] a
-      end else a in
-    if has_std_alignas env ty && has_fun_typ then
-      error loc "alignment specified for function '%s'" id;
-    ((id, add_attributes_type a' ty, init), env1) in
-  (mmap elab_one_name env' namelist, sto, tydef)
 
 (* Elaboration of a field group *)
 
@@ -1706,7 +1684,7 @@ let elab_expr ctx loc env a =
         error "arithmetic on a pointer to an incomplete type %a in binary '%c'" (print_typ env) ty s
   in
 
-  let check_static_var id sto ty =
+  let check_static_var env id sto ty =
     if ctx.ctx_nonstatic_inline
     && sto = Storage_static
     && List.mem AConst (attributes_of_type env ty)
@@ -1720,7 +1698,7 @@ let elab_expr ctx loc env a =
   | VARIABLE s ->
       begin match wrap Env.lookup_ident loc env s with
         | (id, Env.II_ident(sto, ty)) ->
-          check_static_var id sto ty;
+          check_static_var env id sto ty;
           { edesc = EVar id; etyp = ty },env
       | (id, Env.II_enum v) ->
           { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) },env
@@ -1837,7 +1815,7 @@ let elab_expr ctx loc env a =
             emit_elab ~linkage env loc (Gdecl(sto, id, ty, None));
             { edesc = EVar id; etyp = ty },env
         | _ -> elab env a1 in
-      let bl = mmap elab env al in
+      let (bl, env) = mmap elab env al in
       (* Extract type information *)
       let (res, args, vararg) =
         match unroll env b1.etyp with
@@ -1852,14 +1830,19 @@ let elab_expr ctx loc env a =
       (* Type-check the arguments against the prototype *)
       let bl',env =
         match args with
-        | None -> bl
-        | Some proto -> elab_arguments 1 bl proto vararg in
+        | None ->
+          List.iter (fun arg ->
+              let arg_typ = argument_conversion env arg.etyp in
+              if incomplete_type env arg_typ then
+                error "argument type %a is incomplete" (print_typ env) arg.etyp;
+            ) bl; (bl,env)
+        | Some proto -> elab_arguments 1 (bl, env) proto vararg in
       { edesc = ECall(b1, bl'); etyp = res },env
 
   | UNARY(POSINCR, a1) ->
-      elab_pre_post_incr_decr Opostincr "increment" a1
+      elab_pre_post_incr_decr env Opostincr "increment" a1
   | UNARY(POSDECR, a1) ->
-      elab_pre_post_incr_decr Opostdecr "decrement" a1
+      elab_pre_post_incr_decr env Opostdecr "decrement" a1
 
 (* 6.5.4 Cast operators *)
 
@@ -2018,20 +2001,20 @@ let elab_expr ctx loc env a =
       end
 
   | UNARY(PREINCR, a1) ->
-      elab_pre_post_incr_decr Opreincr "increment" a1
+      elab_pre_post_incr_decr env Opreincr "increment" a1
   | UNARY(PREDECR, a1) ->
-      elab_pre_post_incr_decr Opredecr "decrement" a1
+      elab_pre_post_incr_decr env Opredecr "decrement" a1
 
 (* 6.5.5 to 6.5.12  Binary operator expressions *)
 
   | BINARY(MUL, a1, a2) ->
-      elab_binary_arithmetic "*" Omul a1 a2
+      elab_binary_arithmetic env "*" Omul a1 a2
 
   | BINARY(DIV, a1, a2) ->
-      elab_binary_arithmetic "/" Odiv a1 a2
+      elab_binary_arithmetic env "/" Odiv a1 a2
 
   | BINARY(MOD, a1, a2) ->
-      elab_binary_integer "%" Omod a1 a2
+      elab_binary_integer env "%" Omod a1 a2
 
   | BINARY(ADD, a1, a2) ->
       let b1,env = elab env a1 in
@@ -2081,37 +2064,37 @@ let elab_expr ctx loc env a =
       { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres },env
 
   | BINARY(SHL, a1, a2) ->
-      elab_shift "<<" Oshl a1 a2
+      elab_shift env "<<" Oshl a1 a2
 
   | BINARY(SHR, a1, a2) ->
-      elab_shift ">>" Oshr a1 a2
+      elab_shift env ">>" Oshr a1 a2
 
   | BINARY(EQ, a1, a2) ->
-      elab_comparison Oeq a1 a2
+      elab_comparison env Oeq a1 a2
   | BINARY(NE, a1, a2) ->
-      elab_comparison One a1 a2
+      elab_comparison env One a1 a2
   | BINARY(LT, a1, a2) ->
-      elab_comparison Olt a1 a2
+      elab_comparison env Olt a1 a2
   | BINARY(GT, a1, a2) ->
-      elab_comparison Ogt a1 a2
+      elab_comparison env Ogt a1 a2
   | BINARY(LE, a1, a2) ->
-      elab_comparison Ole a1 a2
+      elab_comparison env Ole a1 a2
   | BINARY(GE, a1, a2) ->
-      elab_comparison Oge a1 a2
+      elab_comparison env Oge a1 a2
 
   | BINARY(BAND, a1, a2) ->
-      elab_binary_integer "&" Oand a1 a2
+     elab_binary_integer env "&" Oand a1 a2
   | BINARY(BOR, a1, a2) ->
-      elab_binary_integer "|" Oor a1 a2
+     elab_binary_integer env "|" Oor a1 a2
   | BINARY(XOR, a1, a2) ->
-      elab_binary_integer "^" Oxor a1 a2
+     elab_binary_integer env "^" Oxor a1 a2
 
 (* 6.5.13 and 6.5.14 Logical operator expressions *)
 
   | BINARY(AND, a1, a2) ->
-      elab_logical_operator "&&" Ologand a1 a2
+      elab_logical_operator env "&&" Ologand a1 a2
   | BINARY(OR, a1, a2) ->
-      elab_logical_operator "||" Ologor a1 a2
+      elab_logical_operator env "||" Ologor a1 a2
 
 (* 6.5.15 Conditional expressions *)
   | QUESTION(a1, a2, a3) ->
@@ -2227,7 +2210,7 @@ let elab_expr ctx loc env a =
       { edesc = EBinop (Ocomma, b1, b2, ty2); etyp = ty2 },env
 
 (* Elaboration of pre- or post- increment/decrement *)
-  and elab_pre_post_incr_decr op msg a1 =
+  and elab_pre_post_incr_decr env op msg a1 =
     let b1,env = elab env a1 in
     if not (is_modifiable_lvalue env b1) then
       error "expression is not assignable";
@@ -2236,7 +2219,7 @@ let elab_expr ctx loc env a =
     { edesc = EUnop(op, b1); etyp = b1.etyp },env
 
 (* Elaboration of binary operators over integers *)
-  and elab_binary_integer msg op a1 a2 =
+  and elab_binary_integer env msg op a1 a2 =
     let b1,env = elab env a1 in
     let b2,env = elab env a2 in
     if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then
@@ -2246,7 +2229,7 @@ let elab_expr ctx loc env a =
     { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env
 
 (* Elaboration of binary operators over arithmetic types *)
-  and elab_binary_arithmetic msg op a1 a2 =
+  and elab_binary_arithmetic env msg op a1 a2 =
     let b1,env = elab env a1 in
     let b2,env = elab env a2 in
     if not ((is_arith_type env b1.etyp) && (is_arith_type env b2.etyp)) then
@@ -2256,7 +2239,7 @@ let elab_expr ctx loc env a =
     { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env
 
 (* Elaboration of shift operators *)
-  and elab_shift msg op a1 a2 =
+  and elab_shift env msg op a1 a2 =
     let b1,env = elab env a1 in
     let b2,env = elab env a2 in
     if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then
@@ -2266,7 +2249,7 @@ let elab_expr ctx loc env a =
     { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env
 
 (* Elaboration of comparisons *)
-  and elab_comparison op a1 a2 =
+  and elab_comparison env op a1 a2 =
       let b1,env = elab env a1 in
       let b2,env = elab env a2 in
       let resdesc =
@@ -2303,7 +2286,7 @@ let elab_expr ctx loc env a =
       { edesc = resdesc; etyp = TInt(IInt, []) },env
 
 (* Elaboration of && and || *)
-  and elab_logical_operator msg op a1 a2 =
+  and elab_logical_operator env msg op a1 a2 =
     let b1,env = elab env a1 in
     let b2,env = elab env a2 in
     if not ((is_scalar_type env b1.etyp) && (is_scalar_type env b2.etyp)) then
@@ -2371,113 +2354,101 @@ let __func__type_and_init s =
 
 (* Elaboration of top-level and local definitions *)
 
-let enter_typedefs loc env sto dl =
-  if sto <> Storage_default then
-    error loc "non-default storage class on 'typedef' definition";
-  if dl = [] then
-    warning loc Missing_declarations "typedef requires a name";
-  List.fold_left (fun env (s, ty, init) ->
-    if init <> NO_INIT then
-      error loc "initializer in typedef";
-    if has_std_alignas env ty then
-      error loc "alignment specified for typedef '%s'" s;
-    List.iter
-      (fun a -> match class_of_attribute a with
-                | Attr_object | Attr_struct ->
-                    error loc "attribute '%s' not allowed in 'typedef'"
-                              (name_of_attribute a)
-                | _ -> ())
-      (attributes_of_type_no_expand ty);
-    match previous_def Env.lookup_typedef env s with
-    | Some (s',ty') when Env.in_current_scope env s' ->
-        if equal_types env ty ty' then begin
-          warning loc Celeven_extension "redefinition of typedef '%s' is a C11 extension" s;
-          env
-        end else begin
-          error loc "typedef redefinition with different types (%a vs %a)"
-            (print_typ env) ty (print_typ env) ty';
-          env
-        end
-    | _ ->
-        if redef Env.lookup_ident env s then
-          error loc "redefinition of '%s' as different kind of symbol" s;
-        let (id, env') = Env.enter_typedef env s ty in
-        check_reduced_alignment loc env' ty;
-        emit_elab env loc (Gtypedef(id, ty));
-        env') env dl
-
-let enter_decdefs local nonstatic_inline loc env sto dl =
-  (* Sanity checks on storage class *)
-  if (sto = Storage_auto || sto = Storage_register) && not local then
-    fatal_error loc "illegal storage class %s on file-scoped variable"
-                    (name_of_storage_class sto);
-  if sto <> Storage_default && dl = [] then
-    warning loc Missing_declarations "declaration does not declare anything";
-  let enter_decdef (decls, env) (s, ty, init) =
-    let isfun = is_function_type env ty in
-    if sto = Storage_register && has_std_alignas env ty then
-      error loc "alignment specified for 'register' object '%s'" s;
-    if sto = Storage_extern && init <> NO_INIT then
-      error loc "'extern' declaration variable has an initializer";
-    if local && isfun then begin
-      match sto with
-      | Storage_static ->
-          error loc "function declared in block scope cannot have 'static' storage class"
-      | Storage_auto | Storage_register ->
-          error loc "illegal storage class %s on function"
-                    (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. *)
-    let sto1 =
-      if local && sto = Storage_default && not isfun
-      then Storage_auto
-      else sto in
-    (* enter ident in environment with declared type, because
-       initializer can refer to the ident *)
-    let (id, sto', env1, ty, linkage) =
-      enter_or_refine_ident local loc env s sto1 ty in
-    if init <> NO_INIT && not local then
-      add_global_define loc s;
-    if not isfun && is_void_type env ty then
-      fatal_error loc "'%s' has incomplete type" s;
-    (* process the initializer *)
-    let (ty', init') = elab_initializer loc env1 s ty init in
-    (* update environment with refined type *)
-    let env2 = Env.add_ident env1 id sto' ty' in
-    (* check for incomplete type *)
-    if not isfun && wrap incomplete_type loc env ty' then
-      if not local && sto' = Storage_static then begin
-        warning loc Tentative_incomplete_static "tentative static definition with incomplete type";
-      end else if local && sto' <> Storage_extern then
-        error loc "variable has incomplete type %a" (print_typ env) ty';
-    (* check if alignment is reduced *)
-    check_reduced_alignment loc env ty';
-    (* check for static variables in nonstatic inline functions *)
-    if local && nonstatic_inline
-             && sto' = Storage_static
-             && not (List.mem AConst (attributes_of_type env ty')) then
-      warning loc Static_in_inline "non-constant static local variable '%s' in inline function may be different in different files" s;
-    if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then
-      (* Local definition *)
-      ((sto', id, ty', init') :: decls, env2)
+let enter_typedef loc env sto (s, ty, init) =
+  if init <> NO_INIT then
+    error loc "initializer in typedef";
+  if has_std_alignas env ty then
+    error loc "alignment specified for typedef '%s'" s;
+  List.iter
+    (fun a -> match class_of_attribute a with
+       | Attr_object | Attr_struct ->
+         error loc "attribute '%s' not allowed in 'typedef'"
+           (name_of_attribute a)
+       | _ -> ())
+    (attributes_of_type_no_expand ty);
+  match previous_def Env.lookup_typedef env s with
+  | Some (s',ty') when Env.in_current_scope env s' ->
+    if equal_types env ty ty' then begin
+      warning loc Celeven_extension "redefinition of typedef '%s' is a C11 extension" s;
+      env
+    end
     else begin
-      (* Global definition *)
-      emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init'));
-      (* Make sure the initializer is constant. *)
-      begin match init' with
+      error loc "typedef redefinition with different types (%a vs %a)"
+        (print_typ env) ty (print_typ env) ty';
+      env
+    end
+  | _ ->
+    if redef Env.lookup_ident env s then
+      error loc "redefinition of '%s' as different kind of symbol" s;
+    let (id, env') = Env.enter_typedef env s ty in
+    check_reduced_alignment loc env' ty;
+    emit_elab env loc (Gtypedef(id, ty));
+    env'
+
+let enter_decdef local nonstatic_inline loc sto (decls, env) (s, ty, init) =
+  let isfun = is_function_type env ty in
+  if sto = Storage_register && has_std_alignas env ty then
+    error loc "alignment specified for 'register' object '%s'" s;
+  if sto = Storage_extern && init <> NO_INIT then
+    error loc "'extern' declaration variable has an initializer";
+  if local && isfun then begin
+    match sto with
+    | Storage_static ->
+      error loc "function declared in block scope cannot have 'static' storage class"
+    | Storage_auto | Storage_register ->
+      error loc "illegal storage class %s on function"
+        (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. *)
+  let sto1 =
+    if local && sto = Storage_default && not isfun
+    then Storage_auto
+    else sto in
+  (* enter ident in environment with declared type, because
+     initializer can refer to the ident *)
+  let (id, sto', env1, ty, linkage) =
+    enter_or_refine_ident local loc env s sto1 ty in
+  if init <> NO_INIT && not local then
+    add_global_define loc s;
+  if not isfun && is_void_type env ty then
+    fatal_error loc "'%s' has incomplete type" s;
+  (* process the initializer *)
+  let (ty', init') = elab_initializer loc env1 s ty init in
+  (* update environment with refined type *)
+  let env2 = Env.add_ident env1 id sto' ty' in
+  (* check for incomplete type *)
+  if not isfun && wrap incomplete_type loc env ty' then
+    if not local && sto' = Storage_static then begin
+      warning loc Tentative_incomplete_static "tentative static definition with incomplete type";
+    end
+    else if local && sto' <> Storage_extern then
+      error loc "variable has incomplete type %a" (print_typ env) ty';
+  (* check if alignment is reduced *)
+  check_reduced_alignment loc env ty';
+  (* check for static variables in nonstatic inline functions *)
+  if local && nonstatic_inline
+     && sto' = Storage_static
+     && not (List.mem AConst (attributes_of_type env ty')) then
+    warning loc Static_in_inline "non-constant static local variable '%s' in inline function may be different in different files" s;
+  if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then
+    (* Local definition *)
+    ((sto', id, ty', init') :: decls, env2)
+  else begin
+    (* Global definition *)
+    emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init'));
+    (* Make sure the initializer is constant. *)
+    begin match init' with
       | Some i when not (Ceval.is_constant_init env2 i) ->
-          error loc "initializer is not a compile-time constant"
+        error loc "initializer is not a compile-time constant"
       | _ -> ()
-      end;
-      (decls, env2)
-    end in
-  let (decls, env') = List.fold_left enter_decdef ([], env) dl in
-  (List.rev decls, env')
+    end;
+    (decls, env2)
+  end
 
 (* Processing of K&R-style function definitions.  Synopsis:
       T f(X1, ..., Xn)
@@ -2661,7 +2632,7 @@ let elab_fundef genv spec name defs body loc =
      For prototyped functions this has been done by [elab_fundef_name]
      already, but some parameter may have been shadowed by the
      function name, while it should be the other way around, e.g.
-     [int f(int f) { return f+1; }], with [f] refering to the
+     [int f(int f) { return f+1; }], with [f] referring to the
      parameter [f] and not to the function [f] within the body of the
      function. *)
   let lenv =
@@ -2733,6 +2704,51 @@ let elab_fundef genv spec name defs body loc =
   genv
 
 (* Definitions *)
+let elab_decdef (for_loop: bool) (local: bool) (nonstatic_inline: bool)
+                (env: Env.t) ((spec, namelist): Cabs.init_name_group)
+                (loc: Cabs.cabsloc) : decl list * Env.t =
+  let (sto, inl, noret, tydef, bty, env') =
+    elab_specifier ~only:(namelist=[]) loc env spec in
+  (* Sanity checks on storage class *)
+  if tydef then begin
+    if sto <> Storage_default then
+      error loc "non-default storage class on 'typedef' definition";
+    if namelist = [] then
+      warning loc Missing_declarations "typedef requires a name";
+  end else begin
+    if (sto = Storage_auto || sto = Storage_register) && not local then
+      fatal_error loc "illegal storage class %s on file-scoped variable"
+        (name_of_storage_class sto);
+    if sto <> Storage_default && namelist = [] then
+      warning loc Missing_declarations "declaration does not declare anything";
+  end;
+  let elab_one_name (decls, env) (Init_name (Name (id, decl, attr, loc), init)) =
+    let ((ty, _), env1) =
+      elab_type_declarator loc env bty decl in
+    let a = elab_attributes env attr in
+    let has_fun_typ = is_function_type env ty in
+    if for_loop && (has_fun_typ || sto = Storage_extern || sto = Storage_static || tydef) then
+      error loc "declaration of non-local variable in 'for' loop" ;
+    if has_fun_typ then begin
+      if noret then
+        warning loc Celeven_extension "_Noreturn functions are a C11 extension";
+    end else begin
+      if inl then
+        error loc "'inline' can only appear on functions";
+      if noret then
+        error loc "'_Noreturn' can only appear on functions";
+    end;
+    let a' = if noret then add_attributes [Attr ("noreturn", [])] a else a in
+    if has_std_alignas env ty && has_fun_typ then
+      error loc "alignment specified for function '%s'" id;
+    let decl = (id, add_attributes_type a' ty, init) in
+    if tydef then
+      (decls, enter_typedef loc env1 sto decl)
+    else
+      enter_decdef local nonstatic_inline loc sto (decls, env1) decl
+  in
+  let (decls, env') = List.fold_left elab_one_name ([],env') namelist in
+  (List.rev decls, env')
 
 let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool)
                     (env: Env.t) (def: Cabs.definition)
@@ -2747,18 +2763,7 @@ let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool)
 
   (* "int x = 12, y[10], *z" *)
   | DECDEF(init_name_group, loc) ->
-      let ((dl, env1), sto, tydef) =
-        elab_init_name_group loc env init_name_group in
-      if for_loop then begin
-        let fun_declaration = List.exists (fun (_, ty, _) -> is_function_type env ty) dl in
-        if fun_declaration || sto = Storage_extern || sto = Storage_static || tydef then
-          error loc "declaration of non-local variable in 'for' loop" ;
-      end;
-      if tydef then
-        let env2 = enter_typedefs loc env1 sto dl
-        in ([], env2)
-      else
-        enter_decdefs local nonstatic_inline loc env1 sto dl
+    elab_decdef for_loop local nonstatic_inline env init_name_group loc
 
   (* pragma *)
   | PRAGMA(s, loc) ->
@@ -2885,48 +2890,49 @@ let rec elab_stmt env ctx s =
 (* 6.8.4 Conditional statements *)
 
   | If(a, s1, s2, loc) ->
-      let a',env = elab_expr ctx loc env a in
-      if not (is_scalar_type env a'.etyp) then
+      let a',env' = elab_expr ctx loc (Env.new_scope env) a in
+      if not (is_scalar_type env' a'.etyp) then
         error loc "controlling expression of 'if' does not have scalar type (%a invalid)"
-          (print_typ env) a'.etyp;
-      let s1',env = elab_stmt env ctx s1 in
-      let s2',env =
+          (print_typ env') a'.etyp;
+      let s1' = elab_stmt_new_scope env' ctx s1 in
+      let s2' =
         match s2 with
-          | None -> sskip,env
-          | Some s2 -> elab_stmt env ctx s2
+          | None -> sskip
+          | Some s2 -> elab_stmt_new_scope env' ctx s2
       in
       { sdesc = Sif(a', s1', s2'); sloc = elab_loc loc },env
 
 (* 6.8.5 Iterative statements *)
 
   | WHILE(a, s1, loc) ->
-      let a',env = elab_expr ctx loc env a in
-      if not (is_scalar_type env a'.etyp) then
+      let a',env' = elab_expr ctx loc (Env.new_scope env) a in
+      if not (is_scalar_type env' a'.etyp) then
         error loc "controlling expression of 'while' does not have scalar type (%a invalid)"
-          (print_typ env) a'.etyp;
-      let s1',env = elab_stmt env (ctx_loop ctx) s1 in
+          (print_typ env') a'.etyp;
+      let s1' = elab_stmt_new_scope env' (ctx_loop ctx) s1 in
       { sdesc = Swhile(a', s1'); sloc = elab_loc loc },env
 
   | DOWHILE(a, s1, loc) ->
-      let s1',env = elab_stmt env (ctx_loop ctx) s1 in
-      let a',env = elab_expr ctx loc env a in
-      if not (is_scalar_type env a'.etyp) then
+      let s1' = elab_stmt_new_scope env (ctx_loop ctx) s1 in
+      let a',env' = elab_expr ctx loc (Env.new_scope env) a in
+      if not (is_scalar_type env' a'.etyp) then
         error loc "controlling expression of 'while' does not have scalar type (%a invalid)"
-          (print_typ env) a'.etyp;
+          (print_typ env') a'.etyp;
       { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc },env
 
   | FOR(fc, a2, a3, s1, loc) ->
+      let env' = Env.new_scope env in
       let (a1', env_decls, decls') =
         match fc with
         | Some (FC_EXP a1) ->
-            let a1,env = elab_for_expr ctx loc env (Some a1) in
+            let a1,env = elab_for_expr ctx loc env' (Some a1) in
             (a1, env, None)
         | None ->
-            let a1,env = elab_for_expr ctx loc env None in
+            let a1,env = elab_for_expr ctx loc env' None in
             (a1, env, None)
         | Some (FC_DECL def) ->
             let (dcl, env') = elab_definition true true ctx.ctx_nonstatic_inline
-                                              (Env.new_scope env) def in
+                                              env' def in
             let loc = elab_loc (Cabshelper.get_definitionloc def) in
             (sskip, env',
              Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in
@@ -2938,7 +2944,7 @@ let rec elab_stmt env ctx s =
       if not (is_scalar_type env_test a2'.etyp) then
         error loc "controlling expression of 'for' does not have scalar type (%a invalid)" (print_typ env) a2'.etyp;
       let a3',env_for = elab_for_expr ctx loc env_test a3 in
-      let s1',env_body = elab_stmt env_for (ctx_loop ctx) s1 in
+      let s1' = elab_stmt_new_scope env_for (ctx_loop ctx) s1 in
       let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in
       begin match decls' with
       | None -> sfor,env
@@ -2947,11 +2953,11 @@ let rec elab_stmt env ctx s =
 
 (* 6.8.4 Switch statement *)
   | SWITCH(a, s1, loc) ->
-      let a',env = elab_expr ctx loc env a in
-      if not (is_integer_type env a'.etyp) then
+      let a',env' = elab_expr ctx loc (Env.new_scope env) a in
+      if not (is_integer_type env' a'.etyp) then
         error loc "controlling expression of 'switch' does not have integer type (%a invalid)"
-          (print_typ env) a'.etyp;
-      let s1',env = elab_stmt env (ctx_switch ctx) s1 in
+          (print_typ env') a'.etyp;
+      let s1' = elab_stmt_new_scope env' (ctx_switch ctx) s1 in
       check_switch_cases s1';
       { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env
 
@@ -3025,6 +3031,10 @@ let rec elab_stmt env ctx s =
   | DEFINITION def ->
       error (Cabshelper.get_definitionloc def) "ill-placed definition";
       sskip,env
+(* Elaborate a statement as a block whose scope is a strict subset of the scope
+   of its enclosing block. *)
+and elab_stmt_new_scope env ctx s =
+  fst (elab_stmt (Env.new_scope env) ctx s)
 
 and elab_block loc env ctx b =
   let b',_ = elab_block_body (Env.new_scope env) ctx b in
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index b2a668f0..7cf22eef 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -23,11 +23,18 @@ module SSet = Set.Make(String)
 let lexicon : (string, Cabs.cabsloc -> token) Hashtbl.t = Hashtbl.create 17
 let ignored_keywords : SSet.t ref = ref SSet.empty
 
+let reserved_keyword loc id =
+  Diagnostics.fatal_error (loc.Cabs.filename, loc.Cabs.lineno)
+    "illegal use of reserved keyword `%s'" id
+
 let () =
   List.iter (fun (key, builder) -> Hashtbl.add lexicon key builder)
-    [ ("_Alignas", fun loc -> ALIGNAS loc);
+    [ 
+      ("_Alignas", fun loc -> ALIGNAS loc);
       ("_Alignof", fun loc -> ALIGNOF loc);
       ("_Bool", fun loc -> UNDERSCORE_BOOL loc);
+      ("_Complex", fun loc -> reserved_keyword loc "_Complex");
+      ("_Imaginary", fun loc -> reserved_keyword loc "_Imaginary");
       ("__alignof", fun loc -> ALIGNOF loc);
       ("__alignof__", fun loc -> ALIGNOF loc);
       ("__asm", fun loc -> ASM loc);
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index da8049a5..66b497cc 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -340,7 +340,6 @@ and unblock_block env ctx ploc = function
 
 let unblock_fundef env f =
   local_variables := [];
-  next_scope_id := 0;
   curr_fun_id:= f.fd_name.stamp;
   (* TODO: register the parameters as being declared in function scope *)
   let body = unblock_stmt env [] no_loc f.fd_body in
@@ -398,5 +397,6 @@ let rec unblock_glob env accu = function
 (* Entry point *)
 
 let program p =
+  next_scope_id := 0;
   {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
   unblock_glob (Builtins.environment()) [] p
diff --git a/cparser/handcrafted.messages b/cparser/handcrafted.messages
index 95077739..6d972439 100644
--- a/cparser/handcrafted.messages
+++ b/cparser/handcrafted.messages
@@ -4477,7 +4477,7 @@ translation_unit_file: VOID PRE_NAME TYPEDEF_NAME PACKED LPAREN CONSTANT RPAREN
 ##
 
 # We have just parsed a list of attribute specifiers, but we cannot
-# print it because it is not available. We do not know wether it is
+# print it because it is not available. We do not know whether it is
 # part of the declaration or whether it is part of the first K&R parameter
 # declaration.
 
@@ -4599,7 +4599,7 @@ translation_unit_file: PACKED LPAREN BUILTIN_OFFSETOF XOR_ASSIGN
 ##
 
 Ill-formed __builtin_offsetof.
-At this point, an opening paranthesis '(' is expected.
+At this point, an opening parenthesis '(' is expected.
 
 #------------------------------------------------------------------------------