2011-08-02 Pascal Obry <obry@adacore.com>

	* prj-proc.adb, make.adb, makeutl.adb: Minor reformatting.

2011-08-02  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch5.adb (Expand_Iterator_Loop): Code cleanup and reorganization.
	Set the associated loop as the related expression of internally
	generated cursors.
	* exp_ch7.adb (Is_Container_Cursor): New routine.
	(Wrap_Transient_Declaration): Supress the finalization of the list
	controller when the declaration denotes a container cursor.

2011-08-02  Yannick Moy  <moy@adacore.com>

	* opt.ads (SPARK_Mode): update comment, SPARK_Mode only set through
	command line now.
	* par-ch3.adb (P_Delta_Constraint): remove check in SPARK mode that the
	expression is a simple expression. This check cannot be performed in
	the semantics, so just drop it.
	(P_Index_Or_Discriminant_Constraint): move check that the index or
	discriminant is a subtype mark to Analyze_Subtype_Declaration in the
	semantics. Other cases were previously checked in the semantics.
	* par-ch4.adb (P_Name): move checks that a selector name is not
	character literal or an operator symbol to Find_Selected_Component in
	the semantics
	* par-ch5.adb (Parse_Decls_Begin_End): move check that basic
	declarations are not placed after later declarations in a separate
	procedure in Sem_Util (possibly not the best choice?), to be used both
	during parsing, for Ada 83 mode, and during semantic analysis, for
	SPARK mode.
	* par-endh.adb (Check_End): move check that end label is not missing
	to Process_End_Label in the semantics
	* par-prag.adb (Process_Restrictions_Or_Restriction_Warnings): remove
	the special case for SPARK restriction
	* par.adb: use and with Sem_Util, for use in Parse_Decls_Begin_End
	* restrict.adb, restrict.ads (Check_Formal_Restriction): add a
	parameter Force to issue the error message even on internal node (used
	for generated end label). Call Check_Restriction to check when an error
	must be issued. In SPARK mode, issue an error message even if the
	restriction is not set.
	(Check_Restriction): new procedure with an additional out parameter to
	inform the caller that a message has been issued
	* sem_aggr.adb: Minor modification of message
	* sem_attr.adb (Analyze_Attribute): call Check_Formal_Restriction
	instead of issuing an error message directly
	* sem_ch3.adb (Analyze_Declarations): move here the check that basic
	declarations are not placed after later declarations, by calling
	Check_Later_Vs_Basic_Declarations
	(Analyze_Subtype_Declaration): move here the check that an index or
	discriminant constraint must be a subtype mark. Change the check that
	a subtype of String must start at one so that it works on subtype marks.
	* sem_ch4.adb (Analyze_Call): move here the check that a named
	association cannot follow a positional one in a call
	* sem_ch5.adb (Check_Unreachable_Code): call Check_Formal_Restriction
	instead of issuing an error message directly
	* sem_ch8.adb (Find_Selected_Component): move here the check that a
	selector name is not a character literal or an operator symbol. Move
	here the check that the prefix of an expanded name cannot be a
	subprogram or a loop statement.
	* sem_util.adb, sem_util.ads (Check_Later_Vs_Basic_Declarations): new
	procedure called from parsing and semantics to check that basic
	declarations are not placed after later declarations
	(Process_End_Label): move here the check that end label is not missing

2011-08-02  Arnaud Charlet  <charlet@adacore.com>

	* sem_ch13.adb (Analyze_Enumeration_Representation_Clause): Ignore enum
	representation clause in codepeer mode, since it confuses CodePeer and
	does not bring useful info.

2011-08-02  Ed Falis  <falis@adacore.com>

	* init.c: initialize fp hw on MILS.

2011-08-02  Ed Schonberg  <schonberg@adacore.com>

	* errout.adb (First_Node): for bodies, return the node itself (small
	optimization). For other nodes, do not check source_unit if the node
	comes from Standard.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177151 138bc75d-0d04-0410-961f-82ee72b054a4

26 files changed, 504 insertions, 239 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index cf7374dc8bf..79c2ce742da 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,84 @@
+2011-08-02  Pascal Obry  <obry@adacore.com>
+
+	* prj-proc.adb, make.adb, makeutl.adb: Minor reformatting.
+
+2011-08-02  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch5.adb (Expand_Iterator_Loop): Code cleanup and reorganization.
+	Set the associated loop as the related expression of internally
+	generated cursors.
+	* exp_ch7.adb (Is_Container_Cursor): New routine.
+	(Wrap_Transient_Declaration): Supress the finalization of the list
+	controller when the declaration denotes a container cursor.
+
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* opt.ads (SPARK_Mode): update comment, SPARK_Mode only set through
+	command line now.
+	* par-ch3.adb (P_Delta_Constraint): remove check in SPARK mode that the
+	expression is a simple expression. This check cannot be performed in
+	the semantics, so just drop it.
+	(P_Index_Or_Discriminant_Constraint): move check that the index or
+	discriminant is a subtype mark to Analyze_Subtype_Declaration in the
+	semantics. Other cases were previously checked in the semantics.
+	* par-ch4.adb (P_Name): move checks that a selector name is not
+	character literal or an operator symbol to Find_Selected_Component in
+	the semantics
+	* par-ch5.adb (Parse_Decls_Begin_End): move check that basic
+	declarations are not placed after later declarations in a separate
+	procedure in Sem_Util (possibly not the best choice?), to be used both
+	during parsing, for Ada 83 mode, and during semantic analysis, for
+	SPARK mode.
+	* par-endh.adb (Check_End): move check that end label is not missing
+	to Process_End_Label in the semantics
+	* par-prag.adb (Process_Restrictions_Or_Restriction_Warnings): remove
+	the special case for SPARK restriction
+	* par.adb: use and with Sem_Util, for use in Parse_Decls_Begin_End
+	* restrict.adb, restrict.ads (Check_Formal_Restriction): add a
+	parameter Force to issue the error message even on internal node (used
+	for generated end label). Call Check_Restriction to check when an error
+	must be issued. In SPARK mode, issue an error message even if the
+	restriction is not set.
+	(Check_Restriction): new procedure with an additional out parameter to
+	inform the caller that a message has been issued
+	* sem_aggr.adb: Minor modification of message
+	* sem_attr.adb (Analyze_Attribute): call Check_Formal_Restriction
+	instead of issuing an error message directly
+	* sem_ch3.adb (Analyze_Declarations): move here the check that basic
+	declarations are not placed after later declarations, by calling
+	Check_Later_Vs_Basic_Declarations
+	(Analyze_Subtype_Declaration): move here the check that an index or
+	discriminant constraint must be a subtype mark. Change the check that
+	a subtype of String must start at one so that it works on subtype marks.
+	* sem_ch4.adb (Analyze_Call): move here the check that a named
+	association cannot follow a positional one in a call
+	* sem_ch5.adb (Check_Unreachable_Code): call Check_Formal_Restriction
+	instead of issuing an error message directly
+	* sem_ch8.adb (Find_Selected_Component): move here the check that a
+	selector name is not a character literal or an operator symbol. Move
+	here the check that the prefix of an expanded name cannot be a
+	subprogram or a loop statement.
+	* sem_util.adb, sem_util.ads (Check_Later_Vs_Basic_Declarations): new
+	procedure called from parsing and semantics to check that basic
+	declarations are not placed after later declarations
+	(Process_End_Label): move here the check that end label is not missing
+
+2011-08-02  Arnaud Charlet  <charlet@adacore.com>
+
+	* sem_ch13.adb (Analyze_Enumeration_Representation_Clause): Ignore enum
+	representation clause in codepeer mode, since it confuses CodePeer and
+	does not bring useful info.
+
+2011-08-02  Ed Falis  <falis@adacore.com>
+
+	* init.c: initialize fp hw on MILS.
+
+2011-08-02  Ed Schonberg  <schonberg@adacore.com>
+
+	* errout.adb (First_Node): for bodies, return the node itself (small
+	optimization). For other nodes, do not check source_unit if the node
+	comes from Standard.
+
 2011-08-02  Robert Dewar  <dewar@adacore.com>
 
 	* exp_ch3.adb: Minor comment additions.
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 59babb14581..cfe1d038e1a 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -1332,6 +1332,7 @@ package body Errout is
          --  best to just ignore this situation.
 
          if Loc < Eloc
+           and then Loc /= Standard_Location
            and then Get_Source_File_Index (Loc) = Sfile
          then
             Earliest := Original_Node (N);
@@ -1344,10 +1345,17 @@ package body Errout is
    --  Start of processing for First_Node
 
    begin
-      Earliest := Original_Node (C);
-      Eloc := Sloc (Earliest);
-      Search_Tree_First (Original_Node (C));
-      return Earliest;
+      if Nkind (C) in N_Unit_Body
+        or else Nkind (C) in N_Proper_Body
+      then
+         return C;
+
+      else
+         Earliest := Original_Node (C);
+         Eloc := Sloc (Earliest);
+         Search_Tree_First (Original_Node (C));
+         return Earliest;
+      end if;
    end First_Node;
 
    ----------------
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index 854b1a0ca89..de277662978 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/gcc/ada/exp_ch5.adb
@@ -2859,13 +2859,10 @@ package body Exp_Ch5 is
          --  with the obvious replacements if "reverse" is specified.
 
          declare
-            Element_Type  : constant Entity_Id := Etype (Id);
-            Pack          : constant Entity_Id := Scope (Base_Type (Typ));
-            Name_Init     : Name_Id;
-            Name_Step     : Name_Id;
-            Cond          : Node_Id;
-            Cursor_Decl   : Node_Id;
-            Renaming_Decl : Node_Id;
+            Element_Type : constant Entity_Id := Etype (Id);
+            Pack         : constant Entity_Id := Scope (Base_Type (Typ));
+            Name_Init    : Name_Id;
+            Name_Step    : Name_Id;
 
          begin
             Stats := Statements (N);
@@ -2876,52 +2873,24 @@ package body Exp_Ch5 is
                Cursor := Id;
             end if;
 
-            if Reverse_Present (I_Spec) then
-
-               --  Must verify that the container has a reverse iterator ???
+            --  Must verify that the container has a reverse iterator ???
 
+            if Reverse_Present (I_Spec) then
                Name_Init := Name_Last;
                Name_Step := Name_Previous;
-
             else
                Name_Init := Name_First;
                Name_Step := Name_Next;
             end if;
 
-            --  C : Cursor_Type := Container.First;
-
-            Cursor_Decl :=
-              Make_Object_Declaration (Loc,
-                Defining_Identifier => Cursor,
-                Object_Definition   =>
-                  Make_Selected_Component (Loc,
-                    Prefix        => New_Occurrence_Of (Pack, Loc),
-                    Selector_Name => Make_Identifier (Loc, Name_Cursor)),
-                Expression =>
-                  Make_Selected_Component (Loc,
-                    Prefix        => Relocate_Node (Container),
-                    Selector_Name => Make_Identifier (Loc, Name_Init)));
-
-            Insert_Action (N, Cursor_Decl);
-
-            --  while C /= No_Element loop
-
-            Cond := Make_Op_Ne (Loc,
-                      Left_Opnd  => New_Occurrence_Of (Cursor, Loc),
-                      Right_Opnd => Make_Selected_Component (Loc,
-                         Prefix        => New_Occurrence_Of (Pack, Loc),
-                         Selector_Name =>
-                           Make_Identifier (Loc, Name_No_Element)));
+            --  The code below only handles containers where Element is not a
+            --  primitive operation of the container. This excludes for now the
+            --  Hi-Lite formal containers. Generate:
+            --
+            --    Id : Element_Type renames Container.Element (Cursor);
 
             if Of_Present (I_Spec) then
-
-               --  Id : Element_Type renames Container.Element (Cursor);
-
-               --  The code below only handles containers where Element is not
-               --  a primitive operation of the container. This excludes
-               --  for now the Hi-Lite formal containers.
-
-               Renaming_Decl :=
+               Prepend_To (Stats,
                  Make_Object_Renaming_Declaration (Loc,
                    Defining_Identifier => Id,
                    Subtype_Mark        =>
@@ -2934,9 +2903,7 @@ package body Exp_Ch5 is
                            Selector_Name =>
                              Make_Identifier (Loc, Chars => Name_Element)),
                        Expressions =>
-                         New_List (New_Occurrence_Of (Cursor, Loc))));
-
-               Prepend (Renaming_Decl, Stats);
+                         New_List (New_Occurrence_Of (Cursor, Loc)))));
             end if;
 
             --  For both iterator forms, add call to step operation (Next or
@@ -2951,11 +2918,52 @@ package body Exp_Ch5 is
                 Parameter_Associations =>
                   New_List (New_Occurrence_Of (Cursor, Loc))));
 
-            New_Loop := Make_Loop_Statement (Loc,
-              Iteration_Scheme =>
-                Make_Iteration_Scheme (Loc, Condition => Cond),
-              Statements       => Stats,
-              End_Label        => Empty);
+            --  Generate:
+            --    while Cursor /= No_Element loop
+            --       <Stats>
+            --    end loop;
+
+            New_Loop :=
+              Make_Loop_Statement (Loc,
+                Iteration_Scheme =>
+                  Make_Iteration_Scheme (Loc,
+                    Condition =>
+                      Make_Op_Ne (Loc,
+                        Left_Opnd =>
+                          New_Occurrence_Of (Cursor, Loc),
+                        Right_Opnd =>
+                          Make_Selected_Component (Loc,
+                            Prefix =>
+                              New_Occurrence_Of (Pack, Loc),
+                            Selector_Name =>
+                              Make_Identifier (Loc, Name_No_Element)))),
+                Statements => Stats,
+                End_Label  => Empty);
+
+            --  When the cursor is internally generated, associate it with the
+            --  loop statement.
+
+            if Of_Present (I_Spec) then
+               Set_Ekind (Cursor, E_Variable);
+               Set_Related_Expression (Cursor, New_Loop);
+            end if;
+
+            --  Create the declaration of the cursor and insert it before the
+            --  source loop. Generate:
+            --
+            --    C : Cursor_Type := Container.First;
+
+            Insert_Action (N,
+              Make_Object_Declaration (Loc,
+                Defining_Identifier => Cursor,
+                Object_Definition   =>
+                  Make_Selected_Component (Loc,
+                    Prefix        => New_Occurrence_Of (Pack, Loc),
+                    Selector_Name => Make_Identifier (Loc, Name_Cursor)),
+                Expression =>
+                  Make_Selected_Component (Loc,
+                    Prefix        => Relocate_Node (Container),
+                    Selector_Name => Make_Identifier (Loc, Name_Init))));
 
             --  If the range of iteration is given by a function call that
             --  returns a container, the finalization actions have been saved
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 97ec568e0e9..a344d931879 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -1517,9 +1517,10 @@ package body Exp_Ch7 is
       if Present (Len_Ref) then
          Action :=
            Make_Implicit_If_Statement (N,
-             Condition => Make_Op_Gt (Loc,
-               Left_Opnd  => Len_Ref,
-               Right_Opnd => Make_Integer_Literal (Loc, 0)),
+             Condition =>
+               Make_Op_Gt (Loc,
+                 Left_Opnd  => Len_Ref,
+                 Right_Opnd => Make_Integer_Literal (Loc, 0)),
              Then_Statements => New_List (Action));
       end if;
 
@@ -3417,14 +3418,44 @@ package body Exp_Ch7 is
    --    Finalize_One (_v2);
 
    procedure Wrap_Transient_Declaration (N : Node_Id) is
-      S              : Entity_Id;
-      LC             : Entity_Id := Empty;
-      Nodes          : List_Id;
       Loc            : constant Source_Ptr := Sloc (N);
-      First_Decl_Loc : Source_Ptr;
+      Next_N         : constant Node_Id := Next (N);
       Enclosing_S    : Entity_Id;
+      First_Decl_Loc : Source_Ptr;
+      LC             : Entity_Id := Empty;
+      Nodes          : List_Id;
+      S              : Entity_Id;
       Uses_SS        : Boolean;
-      Next_N         : constant Node_Id := Next (N);
+
+      function Is_Container_Cursor (Decl : Node_Id) return Boolean;
+      --  Determine whether object declaration Decl is a cursor used to iterate
+      --  over an Ada 2005/12 container.
+
+      -------------------------
+      -- Is_Container_Cursor --
+      -------------------------
+
+      function Is_Container_Cursor (Decl : Node_Id) return Boolean is
+         Def_Id : constant Entity_Id := Defining_Identifier (Decl);
+         Expr   : constant Node_Id   := Expression (Decl);
+
+      begin
+         --  A cursor declaration appears in the following form:
+         --
+         --    Index : Pack.Cursor := First (...);
+
+         return
+           Chars (Etype (Def_Id)) = Name_Cursor
+             and then Present (Expr)
+             and then Nkind (Expr) = N_Function_Call
+             and then Chars (Name (Expr)) = Name_First
+             and then
+               (Nkind (Parent (Decl)) = N_Expression_With_Actions
+                  or else
+                Nkind (Related_Expression (Def_Id)) = N_Loop_Statement);
+      end Is_Container_Cursor;
+
+   --  Start of processing for Wrap_Transient_Declaration
 
    begin
       S := Current_Scope;
@@ -3503,6 +3534,29 @@ package body Exp_Ch7 is
          then
             null;
 
+         --  The declaration of a container cursor is a special context where
+         --  the finalization of the list controller needs to be supressed. In
+         --  the following simplified example:
+         --
+         --    LC   : Simple_List_Controller;
+         --    Temp : Ptr_Typ := Container_Creator_Function'Reference;
+         --    Deep_Tag_Attach (Temp, LC);
+         --    Obj  : Pack.Cursor := First (Temp.all);
+         --    Finalize (LC);
+         --    <execute the loop>
+         --
+         --  the finalization of the list controller destroys the contents of
+         --  container Temp, and as a result Obj points to nothing. Note that
+         --  Temp will be finalized by the finalization list of the enclosing
+         --  scope.
+
+         elsif Ada_Version >= Ada_2012
+           and then Is_Container_Cursor (N)
+         then
+            null;
+
+         --  Finalize the list controller
+
          else
             Nodes :=
               Make_Final_Call
diff --git a/gcc/ada/init.c b/gcc/ada/init.c
index 822837c0d19..df0bb932ca7 100644
--- a/gcc/ada/init.c
+++ b/gcc/ada/init.c
@@ -2026,7 +2026,7 @@ __gnat_init_float (void)
      to get correct Ada semantics.  Note that for AE653 vThreads, the HW
      overflow settings are an OS configuration issue.  The instructions
      below have no effect.  */
-#if defined (_ARCH_PPC) && !defined (_SOFT_FLOAT) && !defined (VTHREADS)
+#if defined (_ARCH_PPC) && !defined (_SOFT_FLOAT) && (!defined (VTHREADS) || defined (__VXWORKSMILS__))
 #if defined (__SPE__)
   {
      const unsigned long spefscr_mask = 0xfffffff3;
diff --git a/gcc/ada/make.adb b/gcc/ada/make.adb
index d1fec921953..642281d2fd2 100644
--- a/gcc/ada/make.adb
+++ b/gcc/ada/make.adb
@@ -3823,7 +3823,8 @@ package body Make is
             else
                declare
                   Parent_Directory : constant String :=
-                    Get_Name_String (Project.Directory.Display_Name);
+                                       Get_Name_String
+                                         (Project.Directory.Display_Name);
 
                begin
                   return Parent_Directory & Path_Name;
diff --git a/gcc/ada/makeutl.adb b/gcc/ada/makeutl.adb
index e5c5a9e4bdc..bf352d774eb 100644
--- a/gcc/ada/makeutl.adb
+++ b/gcc/ada/makeutl.adb
@@ -422,7 +422,7 @@ package body Makeutl is
 
                      declare
                         ALI_Path_Name : constant String :=
-                          Name_Buffer (1 .. Name_Len);
+                                          Name_Buffer (1 .. Name_Len);
 
                      begin
                         if Is_Regular_File
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index b05dda45b12..732fc4d97f8 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1887,8 +1887,7 @@ package Opt is
    --  belong to the ALFA subset of Ada. Set by debuf flag -gnatd.F.
 
    SPARK_Mode : Boolean := False;
-   --  Reject constructs not allowed by SPARK. Set by flag -gnatd.D or
-   --  by pragma SPARK_95.
+   --  Reject constructs not allowed by SPARK. Set by flag -gnatd.D.
 
 private
 
diff --git a/gcc/ada/par-ch3.adb b/gcc/ada/par-ch3.adb
index a9cc8c95dda..0d62eb8b0fa 100644
--- a/gcc/ada/par-ch3.adb
+++ b/gcc/ada/par-ch3.adb
@@ -2544,11 +2544,6 @@ package body Ch3 is
       Expr_Node := P_Expression;
       Check_Simple_Expression_In_Ada_83 (Expr_Node);
 
-      if Expr_Form = EF_Non_Simple then
-         Check_Formal_Restriction
-           ("this expression must be parenthesized", Expr_Node);
-      end if;
-
       Set_Delta_Expression (Constraint_Node, Expr_Node);
 
       if Token = Tok_Range then
@@ -3082,12 +3077,6 @@ package body Ch3 is
 
          Expr_Node := P_Expression_Or_Range_Attribute;
 
-         if Expr_Form /= EF_Simple_Name
-           and then Formal_Verification_Mode
-         then
-            Error_Msg_SC ("|~~subtype mark required");
-         end if;
-
          if Expr_Form = EF_Range_Attr then
             Append (Expr_Node, Constr_List);
 
diff --git a/gcc/ada/par-ch4.adb b/gcc/ada/par-ch4.adb
index 338ee641593..4c25c3ca649 100644
--- a/gcc/ada/par-ch4.adb
+++ b/gcc/ada/par-ch4.adb
@@ -209,21 +209,8 @@ package body Ch4 is
          --  designator.
 
          if Token not in Token_Class_Desig then
-
-            --  Selector name cannot be a character literal in SPARK
-
-            if SPARK_Mode and then Token = Tok_Char_Literal then
-               Error_Msg_SC ("|~~character literal cannot be prefixed");
-            end if;
-
             goto Scan_Name_Extension_Dot;
          else
-            --  Selector name cannot be an operator symbol in SPARK
-
-            if SPARK_Mode and then Token = Tok_Operator_Symbol then
-               Error_Msg_SC ("|~~operator symbol cannot be prefixed");
-            end if;
-
             Prefix_Node := Name_Node;
             Name_Node := New_Node (N_Selected_Component, Prev_Token_Ptr);
             Set_Prefix (Name_Node, Prefix_Node);
@@ -682,11 +669,6 @@ package body Ch4 is
             --  Test for => (allow := as error substitute)
 
             if Token = Tok_Arrow or else Token = Tok_Colon_Equal then
-               if SPARK_Mode then
-                  Error_Msg_SP ("|~~no mixing of positional and named "
-                                & "parameter association");
-               end if;
-
                Restore_Scan_State (Scan_State); -- to Id
                goto LP_State_Call;
 
diff --git a/gcc/ada/par-ch5.adb b/gcc/ada/par-ch5.adb
index 3c8f2d5f562..373da1ff6d6 100644
--- a/gcc/ada/par-ch5.adb
+++ b/gcc/ada/par-ch5.adb
@@ -2049,9 +2049,7 @@ package body Ch5 is
 
    procedure Parse_Decls_Begin_End (Parent : Node_Id) is
       Body_Decl    : Node_Id;
-      Body_Sloc    : Source_Ptr;
       Decls        : List_Id;
-      Decl         : Node_Id;
       Parent_Nkind : Node_Kind;
       Spec_Node    : Node_Id;
       HSS          : Node_Id;
@@ -2110,55 +2108,8 @@ package body Ch5 is
    begin
       Decls := P_Declarative_Part;
 
-      --  Check for misplacement of later vs basic declarations in Ada 83.
-      --  The same is true for the SPARK mode: although SPARK 95 removes
-      --  the distinction between initial and later declarative items,
-      --  the distinction remains in the Examiner. (JB01-005)
-      --  Note that the Examiner does not count package declarations in later
-      --  declarative items.
-
-      if Ada_Version = Ada_83 or else SPARK_Mode then
-         Decl := First (Decls);
-
-         --  Loop through sequence of basic declarative items
-
-         Outer : while Present (Decl) loop
-            if Nkind (Decl) /= N_Subprogram_Body
-              and then Nkind (Decl) /= N_Package_Body
-              and then Nkind (Decl) /= N_Task_Body
-              and then Nkind (Decl) not in  N_Body_Stub
-            then
-               Next (Decl);
-
-            --  Once a body is encountered, we only allow later declarative
-            --  items. The inner loop checks the rest of the list.
-
-            else
-               Body_Sloc := Sloc (Decl);
-
-               Inner : while Present (Decl) loop
-                  if (Nkind (Decl) not in N_Later_Decl_Item
-                       or else (SPARK_Mode
-                                 and then
-                                   Nkind (Decl) = N_Package_Declaration))
-                    and then Nkind (Decl) /= N_Pragma
-                  then
-                     if Ada_Version = Ada_83 then
-                        Error_Msg_Sloc := Body_Sloc;
-                        Error_Msg_N
-                          ("(Ada 83) decl cannot appear after body#", Decl);
-                     else
-                        pragma Assert (SPARK_Mode);
-                        Error_Msg_Sloc := Body_Sloc;
-                        Error_Msg_F
-                          ("|~~decl cannot appear after body#", Decl);
-                     end if;
-                  end if;
-
-                  Next (Decl);
-               end loop Inner;
-            end if;
-         end loop Outer;
+      if Ada_Version = Ada_83 then
+         Check_Later_Vs_Basic_Declarations (Decls, During_Parsing => True);
       end if;
 
       --  Here is where we deal with the case of IS used instead of semicolon.
diff --git a/gcc/ada/par-endh.adb b/gcc/ada/par-endh.adb
index 8b0897e1a83..84833cd8dd3 100644
--- a/gcc/ada/par-endh.adb
+++ b/gcc/ada/par-endh.adb
@@ -374,17 +374,6 @@ package body Endh is
                   Set_Comes_From_Source (End_Labl, False);
                   End_Labl_Present := False;
 
-                  --  In SPARK mode, no missing label is allowed
-
-                  if SPARK_Mode
-                    and then End_Type = E_Name
-                    and then Explicit_Start_Label (Scope.Last)
-                  then
-                     Error_Msg_Node_1 := Scope.Table (Scope.Last).Labl;
-                     Error_Msg_SP -- CODEFIX
-                       ("|~~`END &` required");
-                  end if;
-
                   --  Do style check for missing label
 
                   if Style_Check
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 10237a55127..b3dab608a32 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -89,11 +89,11 @@ function Prag (Pragma_Node : Node_Id; Semi : Source_Ptr) return Node_Id is
 
    procedure Process_Restrictions_Or_Restriction_Warnings;
    --  Common processing for Restrictions and Restriction_Warnings pragmas.
-   --  This routine only processes the cases of No_Obsolescent_Features and
-   --  SPARK, which are the only restrictions that have syntactic effects. No
-   --  general error checking is done, since this will be done in Sem_Prag. The
-   --  other case processed is pragma Restrictions No_Dependence, since
-   --  otherwise this is done too late.
+   --  This routine only processes the case of No_Obsolescent_Features, which
+   --  is the only restriction that has syntactic effects. No general error
+   --  checking is done, since this will be done in Sem_Prag. The other case
+   --  processed is pragma Restrictions No_Dependence, since otherwise this is
+   --  done too late.
 
    ----------
    -- Arg1 --
@@ -230,10 +230,6 @@ function Prag (Pragma_Node : Node_Id; Semi : Source_Ptr) return Node_Id is
                   Set_Restriction (No_Obsolescent_Features, Pragma_Node);
                   Restriction_Warnings (No_Obsolescent_Features) :=
                     Prag_Id = Pragma_Restriction_Warnings;
-               when SPARK =>
-                  SPARK_Mode := True;
-                  Set_Error_Msg_Lang ("spark");
-                  Formal_Verification_Mode := True;
                when others =>
                   null;
             end case;
diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb
index 3b0309fbeb6..1f5eb5797bd 100644
--- a/gcc/ada/par.adb
+++ b/gcc/ada/par.adb
@@ -41,6 +41,7 @@ with Par_SCO;  use Par_SCO;
 with Restrict; use Restrict;
 with Scans;    use Scans;
 with Scn;      use Scn;
+with Sem_Util; use Sem_Util;
 with Sinput;   use Sinput;
 with Sinput.L; use Sinput.L;
 with Sinfo;    use Sinfo;
diff --git a/gcc/ada/prj-proc.adb b/gcc/ada/prj-proc.adb
index 0553d33ff8a..f007a718948 100644
--- a/gcc/ada/prj-proc.adb
+++ b/gcc/ada/prj-proc.adb
@@ -2694,7 +2694,6 @@ package body Prj.Proc is
                          Virtual_Prefix
             then
                Project.Virtual := True;
-
             end if;
 
             Project.Path.Display_Name :=
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 215a21f505f..1190f690b21 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -109,24 +109,59 @@ package body Restrict is
    -- Check_Formal_Restriction --
    ------------------------------
 
-   procedure Check_Formal_Restriction (Msg : String; N : Node_Id) is
+   procedure Check_Formal_Restriction
+     (Msg   : String;
+      N     : Node_Id;
+      Force : Boolean := False)
+   is
+      Msg_Issued          : Boolean;
+      Save_Error_Msg_Sloc : Source_Ptr;
    begin
-      if Formal_Verification_Mode
-        and then Comes_From_Source (Original_Node (N))
-      then
-         Error_Msg_F ("|~~" & Msg, N);
+      if Force or else Comes_From_Source (Original_Node (N)) then
+
+         --  Since the call to Restriction_Msg from Check_Restriction may set
+         --  Error_Msg_Sloc to the location of the pragma restriction, save and
+         --  restore the previous value of the global variable around the call.
+
+         --  ??? N in call to Check_Restriction should be First_Node (N), but
+         --  this causes an exception to be raised when analyzing osint.adb.
+         --  To be modified.
+
+         Save_Error_Msg_Sloc := Error_Msg_Sloc;
+         Check_Restriction (Msg_Issued, SPARK, N);  --  N -> First_Node (N)
+         Error_Msg_Sloc := Save_Error_Msg_Sloc;
+
+         if Msg_Issued then
+            Error_Msg_F ("\\| " & Msg, N);
+         elsif SPARK_Mode then
+            Error_Msg_F ("|~~" & Msg, N);
+         end if;
       end if;
    end Check_Formal_Restriction;
 
    procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id) is
+      Msg_Issued          : Boolean;
+      Save_Error_Msg_Sloc : Source_Ptr;
    begin
       pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
 
-      if Formal_Verification_Mode
-        and then Comes_From_Source (Original_Node (N))
-      then
-         Error_Msg_F ("|~~" & Msg1, N);
-         Error_Msg_F (Msg2, N);
+      if Comes_From_Source (Original_Node (N)) then
+
+         --  Since the call to Restriction_Msg from Check_Restriction may set
+         --  Error_Msg_Sloc to the location of the pragma restriction, save and
+         --  restore the previous value of the global variable around the call.
+
+         Save_Error_Msg_Sloc := Error_Msg_Sloc;
+         Check_Restriction (Msg_Issued, SPARK, First_Node (N));
+         Error_Msg_Sloc := Save_Error_Msg_Sloc;
+
+         if Msg_Issued then
+            Error_Msg_F ("\\| " & Msg1, N);
+            Error_Msg_F (Msg2, N);
+         elsif SPARK_Mode then
+            Error_Msg_F ("|~~" & Msg1, N);
+            Error_Msg_F (Msg2, N);
+         end if;
       end if;
    end Check_Formal_Restriction;
 
@@ -256,6 +291,18 @@ package body Restrict is
       N : Node_Id;
       V : Uint := Uint_Minus_1)
    is
+      Msg_Issued : Boolean;
+      pragma Unreferenced (Msg_Issued);
+   begin
+      Check_Restriction (Msg_Issued, R, N, V);
+   end Check_Restriction;
+
+   procedure Check_Restriction
+     (Msg_Issued : out Boolean;
+      R          : Restriction_Id;
+      N          : Node_Id;
+      V          : Uint := Uint_Minus_1)
+   is
       VV : Integer;
       --  V converted to integer form. If V is greater than Integer'Last,
       --  it is reset to minus 1 (unknown value).
@@ -323,6 +370,8 @@ package body Restrict is
    --  Start of processing for Check_Restriction
 
    begin
+      Msg_Issued := False;
+
       --  In CodePeer mode, we do not want to check for any restriction, or set
       --  additional restrictions other than those already set in gnat1drv.adb
       --  so that we have consistency between each compilation.
@@ -386,6 +435,7 @@ package body Restrict is
                    and then Restrictions.Value (R) = 0)
         or else Restrictions.Count (R) > Restrictions.Value (R)
       then
+         Msg_Issued := True;
          Restriction_Msg (R, N);
       end if;
    end Check_Restriction;
diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads
index c006fd6feb1..f0dcb31f275 100644
--- a/gcc/ada/restrict.ads
+++ b/gcc/ada/restrict.ads
@@ -195,11 +195,13 @@ package Restrict is
    --  If a restriction exists post error message at the given node.
 
    procedure Check_Restriction
-     (R : Restriction_Id;
-      N : Node_Id;
-      V : Uint := Uint_Minus_1);
+     (Msg_Issued : out Boolean;
+      R          : Restriction_Id;
+      N          : Node_Id;
+      V          : Uint := Uint_Minus_1);
    --  Checks that the given restriction is not set, and if it is set, an
-   --  appropriate message is posted on the given node. Also records the
+   --  appropriate message is posted on the given node, in which case
+   --  Msg_Issued is set to True (and False otherwise). Also records the
    --  violation in the appropriate internal arrays. Note that it is mandatory
    --  to always use this routine to check if a restriction is violated. Such
    --  checks must never be done directly by the caller, since otherwise
@@ -208,6 +210,13 @@ package Restrict is
    --  indicates the exact count for the violation. If the exact count is not
    --  known, V is left at its default of -1 which indicates an unknown count.
 
+   procedure Check_Restriction
+     (R          : Restriction_Id;
+      N          : Node_Id;
+      V          : Uint := Uint_Minus_1);
+   --  Wrapper on Check_Restriction with Msg_Issued, with the out-parameter
+   --  being ignored here.
+
    procedure Check_Restriction_No_Dependence (U : Node_Id; Err : Node_Id);
    --  Called when a dependence on a unit is created (either implicitly, or by
    --  an explicit WITH clause). U is a node for the unit involved, and Err
@@ -219,11 +228,14 @@ package Restrict is
    --  an elaboration routine. If elaboration code is not allowed, an error
    --  message is posted on the node given as argument.
 
-   procedure Check_Formal_Restriction (Msg : String; N : Node_Id);
+   procedure Check_Formal_Restriction
+     (Msg   : String;
+      N     : Node_Id;
+      Force : Boolean := False);
    --  Node N represents a construct not allowed in formal mode. If this is a
-   --  source node, then an error is issued on N (using Err_Msg_F), prepending
-   --  "|~~" (error not serious, language prepended). Call has no effect if
-   --  not in formal mode, or if N does not come originally from source.
+   --  source node, or if the restriction is forced (Force = True), and the
+   --  SPARK restriction is set, then an error is issued on N. Msg is appended
+   --  to the restriction failure message.
 
    procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id);
    --  Same as Check_Formal_Restriction except there is a continuation message
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 28193ef0ce4..d76c35f7d58 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -3173,7 +3173,7 @@ package body Sem_Aggr is
 
          if Present (Expressions (N)) then
             Check_Formal_Restriction
-              ("named association cannot follow positional association",
+              ("named association cannot follow positional one",
                First (Choices (First (Component_Associations (N)))));
          end if;
 
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 08761d8fd60..4ff4ff4e68c 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -2071,16 +2071,15 @@ package body Sem_Attr is
       --  In SPARK or ALFA, attributes of private types are only allowed if
       --  the full type declaration is visible.
 
-      if Formal_Verification_Mode
-        and then Comes_From_Source (Original_Node (N))
-        and then Is_Entity_Name (P)
+      if Is_Entity_Name (P)
+        and then Present (Entity (P))  --  needed in some cases
         and then Is_Type (Entity (P))
         and then Is_Private_Type (P_Type)
         and then not In_Open_Scopes (Scope (P_Type))
         and then not In_Spec_Expression
       then
-         Error_Msg_FE
-           ("|~~invisible attribute of}", N, First_Subtype (P_Type));
+         Error_Msg_Node_1 := First_Subtype (P_Type);
+         Check_Formal_Restriction ("invisible attribute of}", N);
       end if;
 
       --  Remaining processing depends on attribute
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index a1af56f5aec..901b9e033dc 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -2843,7 +2843,7 @@ package body Sem_Ch13 is
       --  Pointer to node for literal providing max value
 
    begin
-      if Ignore_Rep_Clauses then
+      if Ignore_Rep_Clauses or else CodePeer_Mode then
          return;
       end if;
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 0001ddcef0e..16a6b7dc77f 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1782,7 +1782,7 @@ package body Sem_Ch3 is
       Enter_Name (Id);
 
       if Present (Typ) then
-         if Nkind (Typ) /= N_Identifier then
+         if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then
             Check_Formal_Restriction ("subtype mark required", Typ);
          end if;
 
@@ -2038,6 +2038,10 @@ package body Sem_Ch3 is
    --  Start of processing for Analyze_Declarations
 
    begin
+      if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+         Check_Later_Vs_Basic_Declarations (L, During_Parsing => False);
+      end if;
+
       D := First (L);
       while Present (D) loop
 
@@ -3032,11 +3036,11 @@ package body Sem_Ch3 is
       --  mark and shall not be unconstrained. (The only exception to this
       --  is the admission of declarations of constants of type String.)
 
-      if not Nkind_In (Object_Definition (N), N_Identifier,
-                                              N_Expanded_Name)
+      if not
+        Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name)
       then
          Check_Formal_Restriction
-           ("subtype mark expected", Object_Definition (N));
+           ("subtype mark required", Object_Definition (N));
 
       elsif Is_Array_Type (T)
         and then not Is_Constrained (T)
@@ -3171,7 +3175,9 @@ package body Sem_Ch3 is
 
          if Nkind (Original_Node (N)) = N_Object_Declaration
            and then Comes_From_Source (Original_Node (N))
-           and then Formal_Verification_Mode  --  only call test if needed
+           --  only call test if needed
+           and then (Formal_Verification_Mode
+                      or else Restriction_Check_Required (SPARK))
            and then not Is_SPARK_Initialization_Expr (E)
          then
             Check_Formal_Restriction
@@ -4015,34 +4021,45 @@ package body Sem_Ch3 is
            ("subtype of Boolean cannot have constraint", N);
       end if;
 
-      --  String subtype must have a lower bound of 1 in SPARK/ALFA. Note that
-      --  we do not need to test for the non-static case here, since that was
-      --  already taken care of in Process_Range_Expr_In_Decl.
-
-      if Base_Type (T) = Standard_String
-        and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
-      then
+      if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then
          declare
-            Cstr   : constant Node_Id := Constraint (Subtype_Indication (N));
-            Drange : Node_Id;
-            Low    : Node_Id;
+            Cstr     : constant Node_Id := Constraint (Subtype_Indication (N));
+            One_Cstr : Node_Id;
+            Low      : Node_Id;
+            High     : Node_Id;
 
          begin
-            if Nkind (Cstr) = N_Index_Or_Discriminant_Constraint
-              and then List_Length (Constraints (Cstr)) = 1
-            then
-               Drange := First (Constraints (Cstr));
+            if Nkind (Cstr) = N_Index_Or_Discriminant_Constraint then
+               One_Cstr := First (Constraints (Cstr));
+               while Present (One_Cstr) loop
 
-               if Nkind (Drange) = N_Range then
-                  Low := Low_Bound (Drange);
+                  --  Index or discriminant constraint in SPARK or ALFA must be
+                  --  a subtype mark.
 
-                  if Is_OK_Static_Expression (Low)
-                    and then Expr_Value (Low) /= 1
+                  if not
+                    Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name)
                   then
                      Check_Formal_Restriction
-                       ("String subtype must have lower bound of 1", N);
+                       ("subtype mark required", One_Cstr);
+
+                  --  String subtype must have a lower bound of 1 in SPARK.
+                  --  Note that we do not need to test for the non-static case
+                  --  here, since that was already taken care of in
+                  --  Process_Range_Expr_In_Decl.
+
+                  elsif Base_Type (T) = Standard_String then
+                     Get_Index_Bounds (One_Cstr, Low, High);
+
+                     if Is_OK_Static_Expression (Low)
+                       and then Expr_Value (Low) /= 1
+                     then
+                        Check_Formal_Restriction
+                          ("String subtype must have lower bound of 1", N);
+                     end if;
                   end if;
-               end if;
+
+                  Next (One_Cstr);
+               end loop;
             end if;
          end;
       end if;
@@ -4573,14 +4590,14 @@ package body Sem_Ch3 is
       --  as prefix.
 
       if No (T) then
-         Related_Id :=  Defining_Identifier (P);
+         Related_Id := Defining_Identifier (P);
       else
          Related_Id := T;
       end if;
 
       Nb_Index := 1;
       while Present (Index) loop
-         if Nkind (Index) /= N_Identifier then
+         if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then
             Check_Formal_Restriction ("subtype mark required", Index);
          end if;
 
@@ -4655,7 +4672,7 @@ package body Sem_Ch3 is
       --  Process subtype indication if one is present
 
       if Present (Component_Typ) then
-         if Nkind (Component_Typ) /= N_Identifier then
+         if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
             Check_Formal_Restriction ("subtype mark required", Component_Typ);
          end if;
 
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 4d179d0ebe5..f0b5dd600b0 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -788,6 +788,10 @@ package body Sem_Ch4 is
       --  Flag indicates whether an interpretation of the prefix is a
       --  parameterless call that returns an access_to_subprogram.
 
+      procedure Check_Mixed_Parameter_And_Named_Associations;
+      --  Check that parameter and named associations are not mixed. This is
+      --  a restriction in SPARK mode.
+
       function Name_Denotes_Function return Boolean;
       --  If the type of the name is an access to subprogram, this may be the
       --  type of a name, or the return type of the function being called. If
@@ -798,6 +802,33 @@ package body Sem_Ch4 is
       procedure No_Interpretation;
       --  Output error message when no valid interpretation exists
 
+      --------------------------------------------------
+      -- Check_Mixed_Parameter_And_Named_Associations --
+      --------------------------------------------------
+
+      procedure Check_Mixed_Parameter_And_Named_Associations is
+         Actual     : Node_Id;
+         Named_Seen : Boolean;
+      begin
+         Actual := First (Actuals);
+         Named_Seen := False;
+         while Present (Actual) loop
+            case Nkind (Actual) is
+               when N_Parameter_Association =>
+                  if Named_Seen then
+                     Check_Formal_Restriction
+                       ("named association cannot follow positional one",
+                        Actual);
+                     exit;
+                  end if;
+               when others =>
+                  Named_Seen := True;
+            end case;
+
+            Next (Actual);
+         end loop;
+      end Check_Mixed_Parameter_And_Named_Associations;
+
       ---------------------------
       -- Name_Denotes_Function --
       ---------------------------
@@ -855,6 +886,10 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Call
 
    begin
+      if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+         Check_Mixed_Parameter_And_Named_Associations;
+      end if;
+
       --  Initialize the type of the result of the call to the error type,
       --  which will be reset if the type is successfully resolved.
 
@@ -1887,8 +1922,7 @@ package body Sem_Ch4 is
       ---------------------------
 
       procedure Process_Function_Call is
-         Actual : Node_Id;
-
+         Actual     : Node_Id;
       begin
          Change_Node (N, N_Function_Call);
          Set_Name (N, P);
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 562fad6affa..4c92b6ed0b9 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -37,6 +37,7 @@ with Nlists;   use Nlists;
 with Nmake;    use Nmake;
 with Opt;      use Opt;
 with Restrict; use Restrict;
+with Rident;   use Rident;
 with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
@@ -2501,8 +2502,8 @@ package body Sem_Ch5 is
    ----------------------------
 
    procedure Check_Unreachable_Code (N : Node_Id) is
-      Error_Loc : Source_Ptr;
-      P         : Node_Id;
+      Error_Node : Node_Id;
+      P          : Node_Id;
 
    begin
       if Is_List_Member (N)
@@ -2518,7 +2519,10 @@ package body Sem_Ch5 is
             --  someone could branch to the label, so we just ignore it, unless
             --  we are in formal mode where goto statements are not allowed.
 
-            if Nkind (Nxt) = N_Label and then not Formal_Verification_Mode then
+            if Nkind (Nxt) = N_Label
+              and then not (Formal_Verification_Mode
+                             or else Restriction_Check_Required (SPARK))
+            then
                return;
 
             --  Otherwise see if we have a real statement following us
@@ -2539,7 +2543,7 @@ package body Sem_Ch5 is
                   --  at removing warnings in deleted code, and this is one
                   --  warning we would prefer NOT to have removed.
 
-                  Error_Loc := Sloc (Nxt);
+                  Error_Node := Nxt;
 
                   --  If we have unreachable code, analyze and remove the
                   --  unreachable code, since it is useless and we don't
@@ -2574,11 +2578,11 @@ package body Sem_Ch5 is
 
                   --  Now issue the warning (or error in formal mode)
 
-                  if Formal_Verification_Mode then
-                     Error_Msg
-                       ("|~~unreachable code is not allowed", Error_Loc);
+                  if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+                     Check_Formal_Restriction
+                       ("unreachable code is not allowed", Error_Node);
                   else
-                     Error_Msg ("?unreachable code!", Error_Loc);
+                     Error_Msg ("?unreachable code!", Sloc (Error_Node));
                   end if;
                end if;
 
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 5915ed21b19..a07449c0097 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -5345,13 +5345,26 @@ package body Sem_Ch8 is
 
       if Nkind (P) = N_Error then
          return;
+      end if;
+
+      --  Selector name cannot be a character literal or an operator symbol in
+      --  SPARK.
+
+      if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+         if Nkind (Selector_Name (N)) = N_Character_Literal then
+            Check_Formal_Restriction
+              ("character literal cannot be prefixed", N);
+         elsif Nkind (Selector_Name (N)) = N_Operator_Symbol then
+            Check_Formal_Restriction ("operator symbol cannot be prefixed", N);
+         end if;
+      end if;
 
       --  If the selector already has an entity, the node has been constructed
       --  in the course of expansion, and is known to be valid. Do not verify
       --  that it is defined for the type (it may be a private component used
       --  in the expansion of record equality).
 
-      elsif Present (Entity (Selector_Name (N))) then
+      if Present (Entity (Selector_Name (N))) then
          if No (Etype (N))
            or else Etype (N) = Any_Type
          then
@@ -5474,13 +5487,13 @@ package body Sem_Ch8 is
 
          --  Selector name is restricted in SPARK
 
-         if SPARK_Mode then
+         if SPARK_Mode or else Restriction_Check_Required (SPARK) then
             if Is_Subprogram (P_Name) then
-               Error_Msg_F
-                 ("|~~prefix of expanded name cannot be a subprogram", P);
+               Check_Formal_Restriction
+                 ("prefix of expanded name cannot be a subprogram", P);
             elsif Ekind (P_Name) = E_Loop then
-               Error_Msg_F
-                 ("|~~prefix of expanded name cannot be a loop statement", P);
+               Check_Formal_Restriction
+                 ("prefix of expanded name cannot be a loop statement", P);
             end if;
          end if;
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index bddd50f3dc7..a16c06a7113 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -41,6 +41,7 @@ with Nlists;   use Nlists;
 with Output;   use Output;
 with Opt;      use Opt;
 with Restrict; use Restrict;
+with Rident;   use Rident;
 with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
@@ -1100,6 +1101,61 @@ package body Sem_Util is
       end if;
    end Cannot_Raise_Constraint_Error;
 
+   ---------------------------------------
+   -- Check_Later_Vs_Basic_Declarations --
+   ---------------------------------------
+
+   procedure Check_Later_Vs_Basic_Declarations
+     (Decls          : List_Id;
+      During_Parsing : Boolean)
+   is
+      Body_Sloc : Source_Ptr;
+      Decl      : Node_Id;
+   begin
+      Decl := First (Decls);
+
+      --  Loop through sequence of basic declarative items
+
+      Outer : while Present (Decl) loop
+         if Nkind (Decl) /= N_Subprogram_Body
+           and then Nkind (Decl) /= N_Package_Body
+           and then Nkind (Decl) /= N_Task_Body
+           and then Nkind (Decl) not in N_Body_Stub
+         then
+            Next (Decl);
+
+            --  Once a body is encountered, we only allow later declarative
+            --  items. The inner loop checks the rest of the list.
+
+         else
+            Body_Sloc := Sloc (Decl);
+
+            Inner : while Present (Decl) loop
+               if (Nkind (Decl) not in N_Later_Decl_Item
+                    or else (not During_Parsing
+                              and then
+                                Nkind (Decl) = N_Package_Declaration))
+                 and then Nkind (Decl) /= N_Pragma
+               then
+                  if During_Parsing then
+                     if Ada_Version = Ada_83 then
+                        Error_Msg_Sloc := Body_Sloc;
+                        Error_Msg_N
+                          ("(Ada 83) decl cannot appear after body#", Decl);
+                     end if;
+                  else
+                     Error_Msg_Sloc := Body_Sloc;
+                     Check_Formal_Restriction
+                       ("decl cannot appear after body#", Decl);
+                  end if;
+               end if;
+
+               Next (Decl);
+            end loop Inner;
+         end if;
+      end loop Outer;
+   end Check_Later_Vs_Basic_Declarations;
+
    -----------------------------------------
    -- Check_Dynamically_Tagged_Expression --
    -----------------------------------------
@@ -10478,7 +10534,7 @@ package body Sem_Util is
    procedure Process_End_Label
      (N   : Node_Id;
       Typ : Character;
-      Ent  : Entity_Id)
+      Ent : Entity_Id)
    is
       Loc  : Source_Ptr;
       Nam  : Node_Id;
@@ -10629,6 +10685,18 @@ package body Sem_Util is
 
          Get_Decoded_Name_String (Chars (Endl));
          Set_Sloc (Endl, Sloc (Endl) + Source_Ptr (Name_Len));
+
+      else
+         --  In SPARK mode, no missing label is allowed for packages and
+         --  subprogram bodies. Detect those cases by testing whether
+         --  Process_End_Label was called for a body (Typ = 't') or a package.
+
+         if (SPARK_Mode or else Restriction_Check_Required (SPARK))
+           and then (Typ = 't' or else Ekind (Ent) = E_Package)
+         then
+            Error_Msg_Node_1 := Endl;
+            Check_Formal_Restriction ("`END &` required", Endl, Force => True);
+         end if;
       end if;
 
       --  Now generate the e/t reference
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 471c4a879cc..c52b68a507e 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -146,6 +146,16 @@ package Sem_Util is
    --  not necessarily mean that CE could be raised, but a response of True
    --  means that for sure CE cannot be raised.
 
+   procedure Check_Later_Vs_Basic_Declarations
+     (Decls          : List_Id;
+      During_Parsing : Boolean);
+   --  If During_Parsing is True, check for misplacement of later vs basic
+   --  declarations in Ada 83. If During_Parsing is False, and the SPARK
+   --  restriction is set, do the same: although SPARK 95 removes the
+   --  distinction between initial and later declarative items, the distinction
+   --  remains in the Examiner (JB01-005). Note that the Examiner does not
+   --  count package declarations in later declarative items.
+
    procedure Check_Dynamically_Tagged_Expression
      (Expr        : Node_Id;
       Typ         : Entity_Id;