[multiple changes]

2014-08-04  Yannick Moy  <moy@adacore.com>

	* sem_aggr.adb, sem_ch3.adb, sem_ch5.adb, sem_ch7.adb, sem_ch9.adb,
	sem_ch12.adb, sem_util.adb, sem_util.ads, sem_res.adb, sem_attr.adb,
	exp_ch6.adb, sem_ch4.adb, restrict.adb, restrict.ads, sem_ch6.adb,
	sem_ch8.adb, sem_ch11.adb: Update some subprogram names to refer to
	SPARK_05 instead of SPARK.

2014-08-04  Robert Dewar  <dewar@adacore.com>

	* sem.ads: Minor reformatting.
	* sem_ch13.adb (Analyze_Aspect_External_Or_Link_Name): Minor
	reformatting.
	(Analyze_Aspect_Specifications, case Convention): Put External_Name
	before Link_Name when constructing pragma.

From-SVN: r213537

20 files changed, 225 insertions, 200 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9442616..09575eb 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,21 @@
 2014-08-04  Yannick Moy  <moy@adacore.com>
 
+	* sem_aggr.adb, sem_ch3.adb, sem_ch5.adb, sem_ch7.adb, sem_ch9.adb,
+	sem_ch12.adb, sem_util.adb, sem_util.ads, sem_res.adb, sem_attr.adb,
+	exp_ch6.adb, sem_ch4.adb, restrict.adb, restrict.ads, sem_ch6.adb,
+	sem_ch8.adb, sem_ch11.adb: Update some subprogram names to refer to
+	SPARK_05 instead of SPARK.
+
+2014-08-04  Robert Dewar  <dewar@adacore.com>
+
+	* sem.ads: Minor reformatting.
+	* sem_ch13.adb (Analyze_Aspect_External_Or_Link_Name): Minor
+	reformatting.
+	(Analyze_Aspect_Specifications, case Convention): Put External_Name
+	before Link_Name when constructing pragma.
+
+2014-08-04  Yannick Moy  <moy@adacore.com>
+
 	* sem.adb, sem.ads (In_Default_Expr): Global flag that is set
 	to True during analysis of a default component expression.
 	(Semantics): Save and restore In_Default_Expr around analysis.
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 44488fb..f0b27b4 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -5546,7 +5546,7 @@ package body Exp_Ch6 is
 
       if Nkind (Parent (N)) /= N_Package_Specification then
          if Nkind (Parent (N)) = N_Compilation_Unit then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("subprogram declaration is not a library item", N);
 
          elsif Present (Next (N))
@@ -5560,7 +5560,7 @@ package body Exp_Ch6 is
 
             null;
          else
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("subprogram declaration is not allowed here", N);
          end if;
       end if;
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 9b8e2c6..f2e6a1f 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -491,7 +491,7 @@ package body Restrict is
       --  No_Dispatch restriction is not set.
 
       if R = No_Dispatch then
-         Check_SPARK_Restriction ("class-wide is not allowed", N);
+         Check_SPARK_05_Restriction ("class-wide is not allowed", N);
       end if;
 
       if UI_Is_In_Int_Range (V) then
@@ -1418,11 +1418,11 @@ package body Restrict is
       end if;
    end Set_Restriction_No_Use_Of_Pragma;
 
-   -----------------------------
-   -- Check_SPARK_Restriction --
-   -----------------------------
+   --------------------------------
+   -- Check_SPARK_05_Restriction --
+   --------------------------------
 
-   procedure Check_SPARK_Restriction
+   procedure Check_SPARK_05_Restriction
      (Msg   : String;
       N     : Node_Id;
       Force : Boolean := False)
@@ -1471,9 +1471,9 @@ package body Restrict is
             Error_Msg_F ("\\| " & Msg, N);
          end if;
       end if;
-   end Check_SPARK_Restriction;
+   end Check_SPARK_05_Restriction;
 
-   procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id) is
+   procedure Check_SPARK_05_Restriction (Msg1, Msg2 : String; N : Node_Id) is
       Msg_Issued          : Boolean;
       Save_Error_Msg_Sloc : Source_Ptr;
 
@@ -1500,7 +1500,7 @@ package body Restrict is
             Error_Msg_F (Msg2, N);
          end if;
       end if;
-   end Check_SPARK_Restriction;
+   end Check_SPARK_05_Restriction;
 
    ----------------------------------
    -- Suppress_Restriction_Message --
diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads
index 64a6da1..b16e674 100644
--- a/gcc/ada/restrict.ads
+++ b/gcc/ada/restrict.ads
@@ -258,7 +258,7 @@ package Restrict is
    --  elaboration routine. If elaboration code is not allowed, an error
    --  message is posted on the node given as argument.
 
-   procedure Check_SPARK_Restriction
+   procedure Check_SPARK_05_Restriction
      (Msg   : String;
       N     : Node_Id;
       Force : Boolean := False);
@@ -267,9 +267,9 @@ package Restrict is
    --  the SPARK_05 restriction is set, then an error is issued on N. Msg
    --  is appended to the restriction failure message.
 
-   procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id);
-   --  Same as Check_SPARK_Restriction except there is a continuation message
-   --  Msg2 following the initial message Msg1.
+   procedure Check_SPARK_05_Restriction (Msg1, Msg2 : String; N : Node_Id);
+   --  Same as Check_SPARK_05_Restriction except there is a continuation
+   --  message Msg2 following the initial message Msg1.
 
    procedure Check_No_Implicit_Aliasing (Obj : Node_Id);
    --  Obj is a node for which Is_Aliased_View is True, which is being used in
diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads
index fced125..26c760d 100644
--- a/gcc/ada/sem.ads
+++ b/gcc/ada/sem.ads
@@ -250,13 +250,13 @@ package Sem is
    --  that expression. Probably a boolean would be good enough, since we think
    --  that such expressions cannot nest, but that might not be true in the
    --  future (e.g. if let expressions are added to Ada) so we prepare for that
-   --  future possibility by making it a counter. Like In_Spec_Expression, it
-   --  must be recursively saved on a Semantics call.
+   --  future possibility by making it a counter. As with In_Spec_Expression,
+   --  it must be recursively saved and restored for a Semantics call.
 
    In_Default_Expr : Boolean := False;
    --  Switch to indicate that we are analyzing a default component expression.
-   --  Like In_Spec_Expression, it must be recursively saved on a Semantics
-   --  call.
+   --  As with In_Spec_Expression, it must be recursively saved and restored
+   --  for a Semantics call.
 
    In_Inlined_Body : Boolean := False;
    --  Switch to indicate that we are analyzing and resolving an inlined body.
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 5a0fb10..56c4fad0 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -712,7 +712,7 @@ package body Sem_Aggr is
    begin
       if Level = 0 then
          if Nkind (Parent (Expr)) /= N_Qualified_Expression then
-            Check_SPARK_Restriction ("aggregate should be qualified", Expr);
+            Check_SPARK_05_Restriction ("aggregate should be qualified", Expr);
          end if;
 
       else
@@ -925,12 +925,12 @@ package body Sem_Aggr is
            and then not Is_Constrained (Etype (Name (Parent (N))))
          then
             if not Is_Others_Aggregate (N) then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("array aggregate should have only OTHERS", N);
             end if;
 
          elsif Is_Top_Level_Aggregate (N) then
-            Check_SPARK_Restriction ("aggregate should be qualified", N);
+            Check_SPARK_05_Restriction ("aggregate should be qualified", N);
 
          --  The legality of this unqualified aggregate is checked by calling
          --  Check_Qualified_Aggregate from one of its enclosing aggregate,
@@ -1934,7 +1934,7 @@ package body Sem_Aggr is
                               or else (Nkind (Choice) = N_Range
                                         and then Is_OK_Static_Range (Choice)))
                      then
-                        Check_SPARK_Restriction
+                        Check_SPARK_05_Restriction
                           ("choice should be static", Choice);
                      end if;
                   end if;
@@ -2744,7 +2744,7 @@ package body Sem_Aggr is
       if Is_Entity_Name (A)
         and then Is_Type (Entity (A))
       then
-         Check_SPARK_Restriction ("ancestor part cannot be a type mark", A);
+         Check_SPARK_05_Restriction ("ancestor part cannot be a type mark", A);
 
          --  AI05-0115: if the ancestor part is a subtype mark, the ancestor
          --  must not have unknown discriminants.
@@ -3512,7 +3512,7 @@ package body Sem_Aggr is
       then
 
          if Present (Expressions (N)) then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("named association cannot follow positional one",
                First (Choices (First (Component_Associations (N)))));
          end if;
@@ -3524,13 +3524,13 @@ package body Sem_Aggr is
             Assoc := First (Component_Associations (N));
             while Present (Assoc) loop
                if List_Length (Choices (Assoc)) > 1 then
-                  Check_SPARK_Restriction
+                  Check_SPARK_05_Restriction
                     ("component association in record aggregate must "
                      & "contain a single choice", Assoc);
                end if;
 
                if Nkind (First (Choices (Assoc))) = N_Others_Choice then
-                  Check_SPARK_Restriction
+                  Check_SPARK_05_Restriction
                     ("record aggregate cannot contain OTHERS", Assoc);
                end if;
 
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 2b4cee2..2fab55a 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -320,7 +320,7 @@ package body Sem_Attr is
       --  Verify that prefix of attribute N is a float type and that
       --  two attribute expressions are present
 
-      procedure Check_SPARK_Restriction_On_Attribute;
+      procedure Check_SPARK_05_Restriction_On_Attribute;
       --  Issue an error in formal mode because attribute N is allowed
 
       procedure Check_Integer_Type;
@@ -755,7 +755,7 @@ package body Sem_Attr is
       --  Start of processing for Analyze_Access_Attribute
 
       begin
-         Check_SPARK_Restriction_On_Attribute;
+         Check_SPARK_05_Restriction_On_Attribute;
          Check_E0;
 
          if Nkind (P) = N_Character_Literal then
@@ -1804,14 +1804,14 @@ package body Sem_Attr is
       end Check_Scalar_Type;
 
       ------------------------------------------
-      -- Check_SPARK_Restriction_On_Attribute --
+      -- Check_SPARK_05_Restriction_On_Attribute --
       ------------------------------------------
 
-      procedure Check_SPARK_Restriction_On_Attribute is
+      procedure Check_SPARK_05_Restriction_On_Attribute is
       begin
          Error_Msg_Name_1 := Aname;
-         Check_SPARK_Restriction ("attribute % is not allowed", P);
-      end Check_SPARK_Restriction_On_Attribute;
+         Check_SPARK_05_Restriction ("attribute % is not allowed", P);
+      end Check_SPARK_05_Restriction_On_Attribute;
 
       ---------------------------
       -- Check_Standard_Prefix --
@@ -2556,7 +2556,7 @@ package body Sem_Attr is
         and then not In_Open_Scopes (Scope (P_Type))
         and then not In_Spec_Expression
       then
-         Check_SPARK_Restriction ("invisible attribute of type", N);
+         Check_SPARK_05_Restriction ("invisible attribute of type", N);
       end if;
 
       --  Remaining processing depends on attribute
@@ -2726,7 +2726,7 @@ package body Sem_Attr is
 
          if Nkind (Parent (N)) /= N_Attribute_Reference then
             Error_Msg_Name_1 := Aname;
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("attribute% is only allowed as prefix of another attribute", P);
          end if;
 
@@ -3571,7 +3571,7 @@ package body Sem_Attr is
 
       when Attribute_Image => Image :
       begin
-         Check_SPARK_Restriction_On_Attribute;
+         Check_SPARK_05_Restriction_On_Attribute;
          Check_Scalar_Type;
          Set_Etype (N, Standard_String);
 
@@ -4770,7 +4770,7 @@ package body Sem_Attr is
          if Is_Boolean_Type (P_Type) then
             Error_Msg_Name_1 := Aname;
             Error_Msg_Name_2 := Chars (P_Type);
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("attribute% is not allowed for type%", P);
          end if;
 
@@ -4796,7 +4796,8 @@ package body Sem_Attr is
          if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then
             Error_Msg_Name_1 := Aname;
             Error_Msg_Name_2 := Chars (P_Type);
-            Check_SPARK_Restriction ("attribute% is not allowed for type%", P);
+            Check_SPARK_05_Restriction
+              ("attribute% is not allowed for type%", P);
          end if;
 
          Resolve (E1, P_Base_Type);
@@ -5689,7 +5690,8 @@ package body Sem_Attr is
          if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then
             Error_Msg_Name_1 := Aname;
             Error_Msg_Name_2 := Chars (P_Type);
-            Check_SPARK_Restriction ("attribute% is not allowed for type%", P);
+            Check_SPARK_05_Restriction
+              ("attribute% is not allowed for type%", P);
          end if;
 
          Resolve (E1, P_Base_Type);
@@ -6392,7 +6394,7 @@ package body Sem_Attr is
          if Is_Boolean_Type (P_Type) then
             Error_Msg_Name_1 := Aname;
             Error_Msg_Name_2 := Chars (P_Type);
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("attribute% is not allowed for type%", P);
          end if;
 
@@ -6471,7 +6473,7 @@ package body Sem_Attr is
 
       when Attribute_Value => Value :
       begin
-         Check_SPARK_Restriction_On_Attribute;
+         Check_SPARK_05_Restriction_On_Attribute;
          Check_E1;
          Check_Scalar_Type;
 
@@ -6550,7 +6552,7 @@ package body Sem_Attr is
 
       when Attribute_Wide_Image => Wide_Image :
       begin
-         Check_SPARK_Restriction_On_Attribute;
+         Check_SPARK_05_Restriction_On_Attribute;
          Check_Scalar_Type;
          Set_Etype (N, Standard_Wide_String);
          Check_E1;
@@ -6593,7 +6595,7 @@ package body Sem_Attr is
 
       when Attribute_Wide_Value => Wide_Value :
       begin
-         Check_SPARK_Restriction_On_Attribute;
+         Check_SPARK_05_Restriction_On_Attribute;
          Check_E1;
          Check_Scalar_Type;
 
@@ -6650,7 +6652,7 @@ package body Sem_Attr is
       ----------------
 
       when Attribute_Wide_Width =>
-         Check_SPARK_Restriction_On_Attribute;
+         Check_SPARK_05_Restriction_On_Attribute;
          Check_E0;
          Check_Scalar_Type;
          Set_Etype (N, Universal_Integer);
@@ -6660,7 +6662,7 @@ package body Sem_Attr is
       -----------
 
       when Attribute_Width =>
-         Check_SPARK_Restriction_On_Attribute;
+         Check_SPARK_05_Restriction_On_Attribute;
          Check_E0;
          Check_Scalar_Type;
          Set_Etype (N, Universal_Integer);
diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb
index 21c94bd..45b4a08 100644
--- a/gcc/ada/sem_ch11.adb
+++ b/gcc/ada/sem_ch11.adb
@@ -437,7 +437,7 @@ package body Sem_Ch11 is
          Check_Compiler_Unit ("raise expression", N);
       end if;
 
-      Check_SPARK_Restriction ("raise expression is not allowed", N);
+      Check_SPARK_05_Restriction ("raise expression is not allowed", N);
 
       --  Check exception restrictions on the original source
 
@@ -495,7 +495,7 @@ package body Sem_Ch11 is
 
    begin
       if Comes_From_Source (N) then
-         Check_SPARK_Restriction ("raise statement is not allowed", N);
+         Check_SPARK_05_Restriction ("raise statement is not allowed", N);
       end if;
 
       Check_Unreachable_Code (N);
@@ -702,7 +702,7 @@ package body Sem_Ch11 is
 
    begin
       if Nkind (Original_Node (N)) = N_Raise_Statement then
-         Check_SPARK_Restriction ("raise statement is not allowed", N);
+         Check_SPARK_05_Restriction ("raise statement is not allowed", N);
       end if;
 
       if No (Etype (N)) then
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index ee40fc8..f2e3eca 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -3189,7 +3189,7 @@ package body Sem_Ch12 is
       Decl        : Node_Id;
 
    begin
-      Check_SPARK_Restriction ("generic is not allowed", N);
+      Check_SPARK_05_Restriction ("generic is not allowed", N);
 
       --  We introduce a renaming of the enclosing package, to have a usable
       --  entity as the prefix of an expanded name for a local entity of the
@@ -3322,7 +3322,7 @@ package body Sem_Ch12 is
       Typ         : Entity_Id;
 
    begin
-      Check_SPARK_Restriction ("generic is not allowed", N);
+      Check_SPARK_05_Restriction ("generic is not allowed", N);
 
       --  Create copy of generic unit, and save for instantiation. If the unit
       --  is a child unit, do not copy the specifications for the parent, which
@@ -3618,7 +3618,7 @@ package body Sem_Ch12 is
    --  Start of processing for Analyze_Package_Instantiation
 
    begin
-      Check_SPARK_Restriction ("generic is not allowed", N);
+      Check_SPARK_05_Restriction ("generic is not allowed", N);
 
       --  Very first thing: check for Text_IO sp[ecial unit in case we are
       --  instantiating one of the children of [[Wide_]Wide_]Text_IO.
@@ -4865,7 +4865,7 @@ package body Sem_Ch12 is
    --  Start of processing for Analyze_Subprogram_Instantiation
 
    begin
-      Check_SPARK_Restriction ("generic is not allowed", N);
+      Check_SPARK_05_Restriction ("generic is not allowed", N);
 
       --  Very first thing: check for special Text_IO unit in case we are
       --  instantiating one of the children of [[Wide_]Wide_]Text_IO. Of course
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 85b119b..15bb5b3 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1417,7 +1417,7 @@ package body Sem_Ch13 is
                   if No (A) then
                      Error_Msg_N
                        ("missing Import/Export for Link/External name",
-                         Aspect);
+                        Aspect);
                   end if;
                end;
             end Analyze_Aspect_External_Or_Link_Name;
@@ -1927,14 +1927,14 @@ package body Sem_Ch13 is
 
                      --  Assemble the full argument list
 
-                     if Present (Link_Arg) then
-                        Append_To (Args, Link_Arg);
-                     end if;
-
                      if Present (Extern_Arg) then
                         Append_To (Args, Extern_Arg);
                      end if;
 
+                     if Present (Link_Arg) then
+                        Append_To (Args, Link_Arg);
+                     end if;
+
                      Make_Aitem_Pragma
                        (Pragma_Argument_Associations => Args,
                         Pragma_Name                  => Prag_Nam);
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 0a53fd8..94995d4 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -730,7 +730,7 @@ package body Sem_Ch3 is
       Enclosing_Prot_Type : Entity_Id := Empty;
 
    begin
-      Check_SPARK_Restriction ("access type is not allowed", N);
+      Check_SPARK_05_Restriction ("access type is not allowed", N);
 
       if Is_Entry (Current_Scope)
         and then Is_Task_Type (Etype (Scope (Current_Scope)))
@@ -1053,7 +1053,7 @@ package body Sem_Ch3 is
    --  Start of processing for Access_Subprogram_Declaration
 
    begin
-      Check_SPARK_Restriction ("access type is not allowed", T_Def);
+      Check_SPARK_05_Restriction ("access type is not allowed", T_Def);
 
       --  Associate the Itype node with the inner full-type declaration or
       --  subprogram spec or entry body. This is required to handle nested
@@ -1322,7 +1322,7 @@ package body Sem_Ch3 is
       Full_Desig : Entity_Id;
 
    begin
-      Check_SPARK_Restriction ("access type is not allowed", Def);
+      Check_SPARK_05_Restriction ("access type is not allowed", Def);
 
       --  Check for permissible use of incomplete type
 
@@ -1884,7 +1884,7 @@ package body Sem_Ch3 is
                 (Subtype_Indication (Component_Definition (N)), N);
 
          if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then
-            Check_SPARK_Restriction ("subtype mark required", Typ);
+            Check_SPARK_05_Restriction ("subtype mark required", Typ);
          end if;
 
       --  Ada 2005 (AI-230): Access Definition case
@@ -1937,7 +1937,7 @@ package body Sem_Ch3 is
       --  package Sem).
 
       if Present (E) then
-         Check_SPARK_Restriction ("default expression is not allowed", E);
+         Check_SPARK_05_Restriction ("default expression is not allowed", E);
          Preanalyze_Default_Expression (E, T);
          Check_Initialization (T, E);
 
@@ -2256,7 +2256,7 @@ package body Sem_Ch3 is
          if Nkind (Decl) = N_Package_Declaration
            and then Nkind (Parent (L)) = N_Package_Specification
          then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("package specification cannot contain a package declaration",
                Decl);
          end if;
@@ -2549,7 +2549,7 @@ package body Sem_Ch3 is
 
          when N_Record_Definition =>
             if Present (Discriminant_Specifications (N)) then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("discriminant type is not allowed",
                   Defining_Identifier
                     (First (Discriminant_Specifications (N))));
@@ -2658,7 +2658,7 @@ package body Sem_Ch3 is
       --  Controlled type is not allowed in SPARK
 
       if Is_Visibly_Controlled (T) then
-         Check_SPARK_Restriction ("controlled type is not allowed", N);
+         Check_SPARK_05_Restriction ("controlled type is not allowed", N);
       end if;
 
       --  Some common processing for all types
@@ -2775,7 +2775,7 @@ package body Sem_Ch3 is
       T : Entity_Id;
 
    begin
-      Check_SPARK_Restriction ("incomplete type is not allowed", N);
+      Check_SPARK_05_Restriction ("incomplete type is not allowed", N);
 
       Generate_Definition (Defining_Identifier (N));
 
@@ -3448,14 +3448,14 @@ package body Sem_Ch3 is
       if not
         Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name)
       then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("subtype mark required", Object_Definition (N));
 
       elsif Is_Array_Type (T)
         and then not Is_Constrained (T)
         and then T /= Standard_String
       then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("subtype mark of constrained type expected",
             Object_Definition (N));
       end if;
@@ -3463,7 +3463,7 @@ package body Sem_Ch3 is
       --  There are no aliased objects in SPARK
 
       if Aliased_Present (N) then
-         Check_SPARK_Restriction ("aliased object is not allowed", N);
+         Check_SPARK_05_Restriction ("aliased object is not allowed", N);
       end if;
 
       --  Process initialization expression if present and not in error
@@ -3618,9 +3618,9 @@ package body Sem_Ch3 is
            --  Only call test if needed
 
            and then Restriction_Check_Required (SPARK_05)
-           and then not Is_SPARK_Initialization_Expr (Original_Node (E))
+           and then not Is_SPARK_05_Initialization_Expr (Original_Node (E))
          then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("initialization expression is not appropriate", E);
          end if;
       end if;
@@ -3676,7 +3676,7 @@ package body Sem_Ch3 is
          --  only for constants of type string.
 
          if Is_String_Type (T) and then not Constant_Present (N) then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("declaration of object of unconstrained type not allowed", N);
          end if;
 
@@ -4460,7 +4460,7 @@ package body Sem_Ch3 is
       if Is_Boolean_Type (T)
         and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
       then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("subtype of Boolean cannot have constraint", N);
       end if;
 
@@ -4482,7 +4482,7 @@ package body Sem_Ch3 is
                   if not
                     Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name)
                   then
-                     Check_SPARK_Restriction
+                     Check_SPARK_05_Restriction
                        ("subtype mark required", One_Cstr);
 
                   --  String subtype must have a lower bound of 1 in SPARK.
@@ -4496,7 +4496,7 @@ package body Sem_Ch3 is
                      if Is_OK_Static_Expression (Low)
                        and then Expr_Value (Low) /= 1
                      then
-                        Check_SPARK_Restriction
+                        Check_SPARK_05_Restriction
                           ("String subtype must have lower bound of 1", N);
                      end if;
                   end if;
@@ -4518,7 +4518,7 @@ package body Sem_Ch3 is
          --  in SPARK.
 
          if Is_Array_Type (T) and then not Is_Constrained (T) then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("subtype of unconstrained array must have constraint", N);
          end if;
 
@@ -5092,7 +5092,7 @@ package body Sem_Ch3 is
          --  Check SPARK restriction requiring a subtype mark
 
          if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then
-            Check_SPARK_Restriction ("subtype mark required", Index);
+            Check_SPARK_05_Restriction ("subtype mark required", Index);
          end if;
 
          --  Add a subtype declaration for each index of private array type
@@ -5169,7 +5169,8 @@ package body Sem_Ch3 is
          Set_Etype (Component_Typ, Element_Type);
 
          if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
-            Check_SPARK_Restriction ("subtype mark required", Component_Typ);
+            Check_SPARK_05_Restriction
+              ("subtype mark required", Component_Typ);
          end if;
 
       --  Ada 2005 (AI-230): Access Definition case
@@ -5282,7 +5283,7 @@ package body Sem_Ch3 is
       Set_Packed_Array_Impl_Type (T, Empty);
 
       if Aliased_Present (Component_Definition (Def)) then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("aliased is not allowed", Component_Definition (Def));
          Set_Has_Aliased_Components (Etype (T));
       end if;
@@ -12123,7 +12124,7 @@ package body Sem_Ch3 is
       else
          pragma Assert (Nkind (C) = N_Digits_Constraint);
 
-         Check_SPARK_Restriction ("digits constraint is not allowed", S);
+         Check_SPARK_05_Restriction ("digits constraint is not allowed", S);
 
          Digits_Expr := Digits_Expression (C);
          Analyze_And_Resolve (Digits_Expr, Any_Integer);
@@ -12351,7 +12352,7 @@ package body Sem_Ch3 is
 
       if Nkind (C) = N_Digits_Constraint then
 
-         Check_SPARK_Restriction ("digits constraint is not allowed", S);
+         Check_SPARK_05_Restriction ("digits constraint is not allowed", S);
          Check_Restriction (No_Obsolescent_Features, C);
 
          if Warn_On_Obsolescent_Feature then
@@ -12582,7 +12583,7 @@ package body Sem_Ch3 is
 
       if Nkind (C) = N_Delta_Constraint then
 
-         Check_SPARK_Restriction ("delta constraint is not allowed", S);
+         Check_SPARK_05_Restriction ("delta constraint is not allowed", S);
          Check_Restriction (No_Obsolescent_Features, C);
 
          if Warn_On_Obsolescent_Feature then
@@ -13235,7 +13236,7 @@ package body Sem_Ch3 is
       Bound_Val     : Ureal;
 
    begin
-      Check_SPARK_Restriction
+      Check_SPARK_05_Restriction
         ("decimal fixed point type is not allowed", Def);
       Check_Restriction (No_Fixed_Point, Def);
 
@@ -14790,7 +14791,7 @@ package body Sem_Ch3 is
       --  parent is also an interface.
 
       if Interface_Present (Def) then
-         Check_SPARK_Restriction ("interface is not allowed", Def);
+         Check_SPARK_05_Restriction ("interface is not allowed", Def);
 
          if not Is_Interface (Parent_Type) then
             Diagnose_Interface (Indic, Parent_Type);
@@ -15044,7 +15045,7 @@ package body Sem_Ch3 is
                Defining_Identifier (First (Discriminant_Specifications (N))));
             Set_Has_Discriminants (T, False);
          else
-            Check_SPARK_Restriction ("discriminant type is not allowed", N);
+            Check_SPARK_05_Restriction ("discriminant type is not allowed", N);
          end if;
       end if;
 
@@ -15235,7 +15236,7 @@ package body Sem_Ch3 is
       --  extensions of tagged record types.
 
       if No (Extension) then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("derived type is not allowed", Original_Node (N));
       end if;
    end Derived_Type_Declaration;
@@ -17577,7 +17578,7 @@ package body Sem_Ch3 is
          --  Non-binary case
 
          elsif M_Val < 2 ** Bits then
-            Check_SPARK_Restriction ("modulus should be a power of 2", T);
+            Check_SPARK_05_Restriction ("modulus should be a power of 2", T);
             Set_Non_Binary_Modulus (T);
 
             if Bits > System_Max_Nonbinary_Modulus_Power then
@@ -18507,7 +18508,7 @@ package body Sem_Ch3 is
 
             if Priv_Parent /= Full_Parent then
                Error_Msg_Name_1 := Chars (Priv_Parent);
-               Check_SPARK_Restriction ("% expected", Full_Indic);
+               Check_SPARK_05_Restriction ("% expected", Full_Indic);
             end if;
 
             --  Check the rules of 7.3(10): if the private extension inherits
@@ -19113,7 +19114,7 @@ package body Sem_Ch3 is
          if not In_Iter_Schm
            and then not Is_OK_Static_Range (R)
          then
-            Check_SPARK_Restriction ("range should be static", R);
+            Check_SPARK_05_Restriction ("range should be static", R);
          end if;
 
          Lo := Low_Bound (R);
@@ -20269,11 +20270,11 @@ package body Sem_Ch3 is
         or else not Interface_Present (Def)
       then
          if Limited_Present (Def) then
-            Check_SPARK_Restriction ("limited is not allowed", N);
+            Check_SPARK_05_Restriction ("limited is not allowed", N);
          end if;
 
          if Abstract_Present (Def) then
-            Check_SPARK_Restriction ("abstract is not allowed", N);
+            Check_SPARK_05_Restriction ("abstract is not allowed", N);
          end if;
 
          --  The flag Is_Tagged_Type might have already been set by
@@ -20295,7 +20296,7 @@ package body Sem_Ch3 is
                                       or else Abstract_Present (Def));
 
       else
-         Check_SPARK_Restriction ("interface is not allowed", N);
+         Check_SPARK_05_Restriction ("interface is not allowed", N);
 
          Is_Tagged := True;
          Analyze_Interface_Declaration (T, Def);
@@ -20459,13 +20460,13 @@ package body Sem_Ch3 is
             if Nkind (Ctxt) = N_Package_Body
               and then Nkind (Parent (Ctxt)) = N_Compilation_Unit
             then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("type should be defined in package specification", Typ);
 
             elsif Nkind (Ctxt) /= N_Package_Specification
               or else Nkind (Parent (Parent (Ctxt))) /= N_Compilation_Unit
             then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("type should be defined in library unit package", Typ);
             end if;
          end;
@@ -20494,14 +20495,14 @@ package body Sem_Ch3 is
         or else Null_Present (Component_List (Def))
       then
          if not Is_Tagged_Type (T) then
-            Check_SPARK_Restriction ("untagged record cannot be null", Def);
+            Check_SPARK_05_Restriction ("untagged record cannot be null", Def);
          end if;
 
       else
          Analyze_Declarations (Component_Items (Component_List (Def)));
 
          if Present (Variant_Part (Component_List (Def))) then
-            Check_SPARK_Restriction ("variant part is not allowed", Def);
+            Check_SPARK_05_Restriction ("variant part is not allowed", Def);
             Analyze (Variant_Part (Component_List (Def)));
          end if;
       end if;
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 332bd28..2e1722e 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -403,7 +403,7 @@ package body Sem_Ch4 is
       Onode    : Node_Id;
 
    begin
-      Check_SPARK_Restriction ("allocator is not allowed", N);
+      Check_SPARK_05_Restriction ("allocator is not allowed", N);
 
       --  Deal with allocator restrictions
 
@@ -936,7 +936,7 @@ package body Sem_Ch4 is
             case Nkind (Actual) is
                when N_Parameter_Association =>
                   if Named_Seen then
-                     Check_SPARK_Restriction
+                     Check_SPARK_05_Restriction
                        ("named association cannot follow positional one",
                         Actual);
                      exit;
@@ -1833,7 +1833,7 @@ package body Sem_Ch4 is
       --  source node check, because ???
 
       if Comes_From_Source (N) then
-         Check_SPARK_Restriction ("explicit dereference is not allowed", N);
+         Check_SPARK_05_Restriction ("explicit dereference is not allowed", N);
       end if;
 
       --  In formal verification mode, keep track of all reads and writes
@@ -2052,7 +2052,7 @@ package body Sem_Ch4 is
       end if;
 
       if Comes_From_Source (N) then
-         Check_SPARK_Restriction ("if expression is not allowed", N);
+         Check_SPARK_05_Restriction ("if expression is not allowed", N);
       end if;
 
       Else_Expr := Next (Then_Expr);
@@ -2887,7 +2887,7 @@ package body Sem_Ch4 is
 
    procedure Analyze_Null (N : Node_Id) is
    begin
-      Check_SPARK_Restriction ("null is not allowed", N);
+      Check_SPARK_05_Restriction ("null is not allowed", N);
 
       Set_Etype (N, Any_Access);
    end Analyze_Null;
@@ -3664,7 +3664,7 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Quantified_Expression
 
    begin
-      Check_SPARK_Restriction ("quantified expression is not allowed", N);
+      Check_SPARK_05_Restriction ("quantified expression is not allowed", N);
 
       --  Create a scope to emulate the loop-like behavior of the quantified
       --  expression. The scope is needed to provide proper visibility of the
@@ -4877,7 +4877,7 @@ package body Sem_Ch4 is
 
    begin
       if Comes_From_Source (N) then
-         Check_SPARK_Restriction ("slice is not allowed", N);
+         Check_SPARK_05_Restriction ("slice is not allowed", N);
       end if;
 
       Analyze (P);
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 18a6622..37b62d1 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -893,7 +893,7 @@ package body Sem_Ch5 is
       --  block statements generated by the expander is fine.
 
       if Nkind (Original_Node (N)) = N_Block_Statement then
-         Check_SPARK_Restriction ("block statement is not allowed", N);
+         Check_SPARK_05_Restriction ("block statement is not allowed", N);
       end if;
 
       --  If no handled statement sequence is present, things are really messed
@@ -1212,7 +1212,7 @@ package body Sem_Ch5 is
       --  Case statement with single OTHERS alternative not allowed in SPARK
 
       if Others_Present and then List_Length (Alternatives (N)) = 1 then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("OTHERS as unique case alternative is not allowed", N);
       end if;
 
@@ -1299,7 +1299,7 @@ package body Sem_Ch5 is
 
          else
             if Has_Loop_In_Inner_Open_Scopes (U_Name) then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("exit label must name the closest enclosing loop", N);
             end if;
 
@@ -1343,34 +1343,34 @@ package body Sem_Ch5 is
 
       if Present (Cond) then
          if Nkind (Parent (N)) /= N_Loop_Statement then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("exit with when clause must be directly in loop", N);
          end if;
 
       else
          if Nkind (Parent (N)) /= N_If_Statement then
             if Nkind (Parent (N)) = N_Elsif_Part then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("exit must be in IF without ELSIF", N);
             else
-               Check_SPARK_Restriction ("exit must be directly in IF", N);
+               Check_SPARK_05_Restriction ("exit must be directly in IF", N);
             end if;
 
          elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("exit must be in IF directly in loop", N);
 
          --  First test the presence of ELSE, so that an exit in an ELSE leads
          --  to an error mentioning the ELSE.
 
          elsif Present (Else_Statements (Parent (N))) then
-            Check_SPARK_Restriction ("exit must be in IF without ELSE", N);
+            Check_SPARK_05_Restriction ("exit must be in IF without ELSE", N);
 
          --  An exit in an ELSIF does not reach here, as it would have been
          --  detected in the case (Nkind (Parent (N)) /= N_If_Statement).
 
          elsif Present (Elsif_Parts (Parent (N))) then
-            Check_SPARK_Restriction ("exit must be in IF without ELSIF", N);
+            Check_SPARK_05_Restriction ("exit must be in IF without ELSIF", N);
          end if;
       end if;
 
@@ -1398,7 +1398,7 @@ package body Sem_Ch5 is
       Label_Ent   : Entity_Id;
 
    begin
-      Check_SPARK_Restriction ("goto statement is not allowed", N);
+      Check_SPARK_05_Restriction ("goto statement is not allowed", N);
 
       --  Actual semantic checks
 
@@ -2481,7 +2481,7 @@ package body Sem_Ch5 is
       --  Loop parameter specification must include subtype mark in SPARK
 
       if Nkind (DS) = N_Range then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("loop parameter specification must include subtype mark", N);
       end if;
 
@@ -3348,7 +3348,7 @@ package body Sem_Ch5 is
                   --  Now issue the warning (or error in formal mode)
 
                   if Restriction_Check_Required (SPARK_05) then
-                     Check_SPARK_Restriction
+                     Check_SPARK_05_Restriction
                        ("unreachable code is not allowed", Error_Node);
                   else
                      Error_Msg ("??unreachable code!", Sloc (Error_Node));
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index e6e35ab..0997873 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -213,7 +213,7 @@ package body Sem_Ch6 is
       Scop       : constant Entity_Id := Current_Scope;
 
    begin
-      Check_SPARK_Restriction ("abstract subprogram is not allowed", N);
+      Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
 
       Generate_Definition (Designator);
       Set_Contract (Designator, Make_Contract (Sloc (Designator)));
@@ -882,12 +882,12 @@ package body Sem_Ch6 is
              (Nkind (Parent (Parent (N))) /= N_Subprogram_Body
                or else Present (Next (N)))
          then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("RETURN should be the last statement in function", N);
          end if;
 
       else
-         Check_SPARK_Restriction ("extended RETURN is not allowed", N);
+         Check_SPARK_05_Restriction ("extended RETURN is not allowed", N);
 
          --  Analyze parts specific to extended_return_statement:
 
@@ -1861,7 +1861,7 @@ package body Sem_Ch6 is
 
       if Result_Definition (N) /= Error then
          if Nkind (Result_Definition (N)) = N_Access_Definition then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("access result is not allowed", Result_Definition (N));
 
             --  Ada 2005 (AI-254): Handle anonymous access to subprograms
@@ -1895,7 +1895,7 @@ package body Sem_Ch6 is
             --  Unconstrained array as result is not allowed in SPARK
 
             if Is_Array_Type (Typ) and then not Is_Constrained (Typ) then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("returning an unconstrained array is not allowed",
                   Result_Definition (N));
             end if;
@@ -2674,7 +2674,7 @@ package body Sem_Ch6 is
                  and then not Nkind_In (Stat, N_Simple_Return_Statement,
                                               N_Extended_Return_Statement)
                then
-                  Check_SPARK_Restriction
+                  Check_SPARK_05_Restriction
                     ("last statement in function should be RETURN", Stat);
                end if;
             end;
@@ -2692,7 +2692,7 @@ package body Sem_Ch6 is
             --  borrow the Check_Returns procedure here ???
 
             if Return_Present (Id) then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("procedure should not have RETURN", N);
             end if;
          end if;
@@ -4144,7 +4144,7 @@ package body Sem_Ch6 is
       if Nkind (Specification (N)) = N_Procedure_Specification
         and then Null_Present (Specification (N))
       then
-         Check_SPARK_Restriction ("null procedure is not allowed", N);
+         Check_SPARK_05_Restriction ("null procedure is not allowed", N);
 
          if Is_Protected_Type (Current_Scope) then
             Error_Msg_N ("protected operation cannot be a null procedure", N);
@@ -4351,7 +4351,8 @@ package body Sem_Ch6 is
       if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
         and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration
       then
-         Check_SPARK_Restriction ("user-defined operator is not allowed", N);
+         Check_SPARK_05_Restriction
+           ("user-defined operator is not allowed", N);
       end if;
 
       --  Proceed with analysis. Do not emit a cross-reference entry if the
@@ -9771,7 +9772,7 @@ package body Sem_Ch6 is
 
          if Nkind (S) /= N_Defining_Operator_Symbol then
             Error_Msg_Sloc := Sloc (Homonym (S));
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("overloading not allowed with entity#", S);
          end if;
 
@@ -10081,7 +10082,7 @@ package body Sem_Ch6 is
          Default := Expression (Param_Spec);
 
          if Present (Default) then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("default expression is not allowed", Default);
 
             if Out_Present (Param_Spec) then
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 163c845..722825e 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -1093,7 +1093,7 @@ package body Sem_Ch7 is
 
                   else
                      Error_Msg_Sloc := Sloc (Previous);
-                     Check_SPARK_Restriction
+                     Check_SPARK_05_Restriction
                        ("at most one tagged type or type extension allowed",
                         "\\ previous declaration#",
                         Decl);
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 0780f3f..251fc43 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -552,7 +552,7 @@ package body Sem_Ch8 is
       Nam : constant Node_Id := Name (N);
 
    begin
-      Check_SPARK_Restriction ("exception renaming is not allowed", N);
+      Check_SPARK_05_Restriction ("exception renaming is not allowed", N);
 
       Enter_Name (Id);
       Analyze (Nam);
@@ -658,7 +658,7 @@ package body Sem_Ch8 is
          return;
       end if;
 
-      Check_SPARK_Restriction ("generic renaming is not allowed", N);
+      Check_SPARK_05_Restriction ("generic renaming is not allowed", N);
 
       Generate_Definition (New_P);
 
@@ -836,7 +836,7 @@ package body Sem_Ch8 is
          return;
       end if;
 
-      Check_SPARK_Restriction ("object renaming is not allowed", N);
+      Check_SPARK_05_Restriction ("object renaming is not allowed", N);
 
       Set_Is_Pure (Id, Is_Pure (Current_Scope));
       Enter_Name (Id);
@@ -3430,7 +3430,7 @@ package body Sem_Ch8 is
    --  Start of processing for Analyze_Use_Package
 
    begin
-      Check_SPARK_Restriction ("use clause is not allowed", N);
+      Check_SPARK_05_Restriction ("use clause is not allowed", N);
 
       Set_Hidden_By_Use_Clause (N, No_Elist);
 
@@ -6392,12 +6392,13 @@ package body Sem_Ch8 is
 
       if Restriction_Check_Required (SPARK_05) then
          if Nkind (Selector_Name (N)) = N_Character_Literal then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("character literal cannot be prefixed", N);
          elsif Nkind (Selector_Name (N)) = N_Operator_Symbol
            and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration
          then
-            Check_SPARK_Restriction ("operator symbol cannot be prefixed", N);
+            Check_SPARK_05_Restriction
+              ("operator symbol cannot be prefixed", N);
          end if;
       end if;
 
@@ -6765,10 +6766,10 @@ package body Sem_Ch8 is
            and then Restriction_Check_Required (SPARK_05)
          then
             if Is_Subprogram (P_Name) then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("prefix of expanded name cannot be a subprogram", P);
             elsif Ekind (P_Name) = E_Loop then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("prefix of expanded name cannot be a loop statement", P);
             end if;
          end if;
@@ -6927,7 +6928,7 @@ package body Sem_Ch8 is
 
          elsif Attribute_Name (N) = Name_Base then
             Error_Msg_Name_1 := Name_Base;
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("attribute% is only allowed as prefix of another attribute", N);
 
             if Ada_Version = Ada_83 and then Comes_From_Source (N) then
diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb
index 7a49d4b..6be4f55 100644
--- a/gcc/ada/sem_ch9.adb
+++ b/gcc/ada/sem_ch9.adb
@@ -701,7 +701,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("abort statement is not allowed", N);
+      Check_SPARK_05_Restriction ("abort statement is not allowed", N);
 
       T_Name := First (Names (N));
       while Present (T_Name) loop
@@ -772,7 +772,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("accept statement is not allowed", N);
+      Check_SPARK_05_Restriction ("accept statement is not allowed", N);
 
       --  Entry name is initialized to Any_Id. It should get reset to the
       --  matching entry entity. An error is signalled if it is not reset.
@@ -1003,7 +1003,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("select statement is not allowed", N);
+      Check_SPARK_05_Restriction ("select statement is not allowed", N);
       Check_Restriction (Max_Asynchronous_Select_Nesting, N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -1049,7 +1049,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("select statement is not allowed", N);
+      Check_SPARK_05_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
       --  Ada 2005 (AI-345): The trigger may be a dispatching call
@@ -1146,7 +1146,7 @@ package body Sem_Ch9 is
       E : constant Node_Id := Expression (N);
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("delay statement is not allowed", N);
+      Check_SPARK_05_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Relative_Delay, N);
       Check_Restriction (No_Delay, N);
       Check_Potentially_Blocking_Operation (N);
@@ -1164,7 +1164,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("delay statement is not allowed", N);
+      Check_SPARK_05_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Delay, N);
       Check_Potentially_Blocking_Operation (N);
       Analyze (E);
@@ -1453,7 +1453,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("entry call is not allowed", N);
+      Check_SPARK_05_Restriction ("entry call is not allowed", N);
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
@@ -1886,7 +1886,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("protected definition is not allowed", N);
+      Check_SPARK_05_Restriction ("protected definition is not allowed", N);
       Analyze_Declarations (Visible_Declarations (N));
 
       if Present (Private_Declarations (N))
@@ -2176,7 +2176,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("requeue statement is not allowed", N);
+      Check_SPARK_05_Restriction ("requeue statement is not allowed", N);
       Check_Restriction (No_Requeue_Statements, N);
       Check_Unreachable_Code (N);
 
@@ -2471,7 +2471,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("select statement is not allowed", N);
+      Check_SPARK_05_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
       --  Loop to analyze alternatives
@@ -2862,7 +2862,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("task definition is not allowed", N);
+      Check_SPARK_05_Restriction ("task definition is not allowed", N);
 
       if Present (Visible_Declarations (N)) then
          Analyze_Declarations (Visible_Declarations (N));
@@ -3045,7 +3045,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_SPARK_Restriction ("select statement is not allowed", N);
+      Check_SPARK_05_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
       --  Ada 2005 (AI-345): The trigger may be a dispatching call
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 22e6fd6..b7fa5f5 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3885,7 +3885,7 @@ package body Sem_Res is
                --  conversions of objects), not general expressions.
 
                if Is_Actual_Tagged_Parameter (A) then
-                  if Is_SPARK_Object_Reference (A) then
+                  if Is_SPARK_05_Object_Reference (A) then
                      null;
 
                   elsif Nkind (A) = N_Type_Conversion then
@@ -3895,8 +3895,8 @@ package body Sem_Res is
                         Target_Typ  : constant Entity_Id := A_Typ;
 
                      begin
-                        if not Is_SPARK_Object_Reference (Operand) then
-                           Check_SPARK_Restriction
+                        if not Is_SPARK_05_Object_Reference (Operand) then
+                           Check_SPARK_05_Restriction
                              ("object required", Operand);
 
                         --  In formal mode, the only view conversions are those
@@ -3912,11 +3912,11 @@ package body Sem_Res is
                            if Ekind_In
                              (F, E_Out_Parameter, E_In_Out_Parameter)
                            then
-                              Check_SPARK_Restriction
+                              Check_SPARK_05_Restriction
                                 ("ancestor conversion is the only permitted "
                                  & "view conversion", A);
                            else
-                              Check_SPARK_Restriction
+                              Check_SPARK_05_Restriction
                                 ("ancestor conversion required", A);
                            end if;
 
@@ -3926,7 +3926,7 @@ package body Sem_Res is
                      end;
 
                   else
-                     Check_SPARK_Restriction ("object required", A);
+                     Check_SPARK_05_Restriction ("object required", A);
                   end if;
 
                --  In formal mode, the only view conversions are those
@@ -3935,7 +3935,7 @@ package body Sem_Res is
                elsif Nkind (A) = N_Type_Conversion
                  and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
                then
-                  Check_SPARK_Restriction
+                  Check_SPARK_05_Restriction
                     ("ancestor conversion is the only permitted view "
                      & "conversion", A);
                end if;
@@ -5238,7 +5238,7 @@ package body Sem_Res is
         and then
           not Nkind_In (Parent (N), N_Qualified_Expression, N_Type_Conversion)
       then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("operation should be qualified or explicitly converted", N);
       end if;
 
@@ -5610,7 +5610,7 @@ package body Sem_Res is
 
         and then Ekind (Nam) /= E_Enumeration_Literal
       then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("call to subprogram cannot appear before its body", N);
       end if;
 
@@ -5780,7 +5780,7 @@ package body Sem_Res is
          if Restriction_Check_Required (SPARK_05)
            and then Same_Or_Aliased_Subprograms (Nam, Scop)
          then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("subprogram may not contain direct call to itself", N);
          end if;
 
@@ -6149,7 +6149,7 @@ package body Sem_Res is
         and then Is_Entity_Name (Name (N))
         and then Is_Inherited_Operation_For_Type (Entity (Name (N)), Etype (N))
       then
-         Check_SPARK_Restriction ("function not inherited", N);
+         Check_SPARK_05_Restriction ("function not inherited", N);
       end if;
 
       --  Implement rule in 12.5.1 (23.3/2): In an instance, if the actual is
@@ -6462,13 +6462,13 @@ package body Sem_Res is
       --  types or array types except String.
 
       if Is_Boolean_Type (T) then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("comparison is not defined on Boolean type", N);
 
       elsif Is_Array_Type (T)
         and then Base_Type (T) /= Standard_String
       then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("comparison is not defined on array types other than String", N);
       end if;
 
@@ -7514,7 +7514,7 @@ package body Sem_Res is
               and then Etype (R) /= Any_Composite  --  or else R in error
               and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
             then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("array types should have matching static bounds", N);
             end if;
          end if;
@@ -8272,7 +8272,7 @@ package body Sem_Res is
               and then Right_Typ /= Any_Composite  --  or Right_Opnd in error
               and then not Matching_Static_Array_Bounds (Left_Typ, Right_Typ)
             then
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("array types should have matching static bounds", N);
             end if;
          end;
@@ -8571,7 +8571,7 @@ package body Sem_Res is
       end loop;
 
       if Base_Type (Etype (N)) /= Standard_String then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("result of concatenation should have type String", N);
       end if;
    end Resolve_Op_Concat;
@@ -8706,7 +8706,7 @@ package body Sem_Res is
 
       if Is_Character_Type (Etype (Arg)) then
          if not Is_OK_Static_Expression (Arg) then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("character operand for concatenation should be static", Arg);
          end if;
 
@@ -8715,7 +8715,7 @@ package body Sem_Res is
                   and then Is_Constant_Object (Entity (Arg)))
            and then not Is_OK_Static_Expression (Arg)
          then
-            Check_SPARK_Restriction
+            Check_SPARK_05_Restriction
               ("string operand for concatenation should be static", Arg);
          end if;
 
@@ -9026,7 +9026,7 @@ package body Sem_Res is
         and then Etype (Expr) /= Any_Composite  --  or else Expr in error
         and then not Matching_Static_Array_Bounds (Target_Typ, Etype (Expr))
       then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("array types should have matching static bounds", N);
       end if;
 
@@ -10235,7 +10235,7 @@ package body Sem_Res is
         and then Operand_Typ /= Any_Composite  --  or else Operand in error
         and then not Matching_Static_Array_Bounds (Target_Typ, Operand_Typ)
       then
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("array types should have matching static bounds", N);
       end if;
 
@@ -10247,9 +10247,9 @@ package body Sem_Res is
         and then Is_Tagged_Type (Operand_Typ)
         and then not Is_Class_Wide_Type (Operand_Typ)
         and then Is_Ancestor (Target_Typ, Operand_Typ)
-        and then not Is_SPARK_Object_Reference (Operand)
+        and then not Is_SPARK_05_Object_Reference (Operand)
       then
-         Check_SPARK_Restriction ("object required", Operand);
+         Check_SPARK_05_Restriction ("object required", Operand);
       end if;
 
       Analyze_Dimension (N);
@@ -10520,7 +10520,7 @@ package body Sem_Res is
    begin
       if Is_Modular_Integer_Type (Typ) and then Nkind (N) /= N_Op_Not then
          Error_Msg_Name_1 := Chars (Typ);
-         Check_SPARK_Restriction
+         Check_SPARK_05_Restriction
            ("unary operator not defined for modular type%", N);
       end if;
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 8bbf48c..4c8bddd 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -2557,7 +2557,7 @@ package body Sem_Util is
                      end if;
                   else
                      Error_Msg_Sloc := Body_Sloc;
-                     Check_SPARK_Restriction
+                     Check_SPARK_05_Restriction
                        ("decl cannot appear after body#", Decl);
                   end if;
                end if;
@@ -5426,7 +5426,7 @@ package body Sem_Util is
               and then Comes_From_Source (C)
             then
                Error_Msg_Sloc := Sloc (C);
-               Check_SPARK_Restriction
+               Check_SPARK_05_Restriction
                  ("redeclaration of identifier &#", Def_Id);
             end if;
          end;
@@ -11459,11 +11459,11 @@ package body Sem_Util is
       end if;
    end Is_Selector_Name;
 
-   ----------------------------------
-   -- Is_SPARK_Initialization_Expr --
-   ----------------------------------
+   -------------------------------------
+   -- Is_SPARK_05_Initialization_Expr --
+   -------------------------------------
 
-   function Is_SPARK_Initialization_Expr (N : Node_Id) return Boolean is
+   function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean is
       Is_Ok     : Boolean;
       Expr      : Node_Id;
       Comp_Assn : Node_Id;
@@ -11507,27 +11507,28 @@ package body Sem_Util is
 
          when N_Qualified_Expression |
               N_Type_Conversion      =>
-            Is_Ok := Is_SPARK_Initialization_Expr (Expression (Orig_N));
+            Is_Ok := Is_SPARK_05_Initialization_Expr (Expression (Orig_N));
 
          when N_Unary_Op =>
-            Is_Ok := Is_SPARK_Initialization_Expr (Right_Opnd (Orig_N));
+            Is_Ok := Is_SPARK_05_Initialization_Expr (Right_Opnd (Orig_N));
 
          when N_Binary_Op       |
               N_Short_Circuit   |
               N_Membership_Test =>
-            Is_Ok := Is_SPARK_Initialization_Expr (Left_Opnd (Orig_N))
+            Is_Ok := Is_SPARK_05_Initialization_Expr (Left_Opnd (Orig_N))
                        and then
-                         Is_SPARK_Initialization_Expr (Right_Opnd (Orig_N));
+                         Is_SPARK_05_Initialization_Expr (Right_Opnd (Orig_N));
 
          when N_Aggregate           |
               N_Extension_Aggregate =>
             if Nkind (Orig_N) = N_Extension_Aggregate then
-               Is_Ok := Is_SPARK_Initialization_Expr (Ancestor_Part (Orig_N));
+               Is_Ok :=
+                 Is_SPARK_05_Initialization_Expr (Ancestor_Part (Orig_N));
             end if;
 
             Expr := First (Expressions (Orig_N));
             while Present (Expr) loop
-               if not Is_SPARK_Initialization_Expr (Expr) then
+               if not Is_SPARK_05_Initialization_Expr (Expr) then
                   Is_Ok := False;
                   goto Done;
                end if;
@@ -11539,7 +11540,7 @@ package body Sem_Util is
             while Present (Comp_Assn) loop
                Expr := Expression (Comp_Assn);
                if Present (Expr)  --  needed for box association
-                 and then not Is_SPARK_Initialization_Expr (Expr)
+                 and then not Is_SPARK_05_Initialization_Expr (Expr)
                then
                   Is_Ok := False;
                   goto Done;
@@ -11550,12 +11551,12 @@ package body Sem_Util is
 
          when N_Attribute_Reference =>
             if Nkind (Prefix (Orig_N)) in N_Subexpr then
-               Is_Ok := Is_SPARK_Initialization_Expr (Prefix (Orig_N));
+               Is_Ok := Is_SPARK_05_Initialization_Expr (Prefix (Orig_N));
             end if;
 
             Expr := First (Expressions (Orig_N));
             while Present (Expr) loop
-               if not Is_SPARK_Initialization_Expr (Expr) then
+               if not Is_SPARK_05_Initialization_Expr (Expr) then
                   Is_Ok := False;
                   goto Done;
                end if;
@@ -11575,13 +11576,13 @@ package body Sem_Util is
 
    <<Done>>
       return Is_Ok;
-   end Is_SPARK_Initialization_Expr;
+   end Is_SPARK_05_Initialization_Expr;
 
-   -------------------------------
-   -- Is_SPARK_Object_Reference --
-   -------------------------------
+   ----------------------------------
+   -- Is_SPARK_05_Object_Reference --
+   ----------------------------------
 
-   function Is_SPARK_Object_Reference (N : Node_Id) return Boolean is
+   function Is_SPARK_05_Object_Reference (N : Node_Id) return Boolean is
    begin
       if Is_Entity_Name (N) then
          return Present (Entity (N))
@@ -11592,13 +11593,13 @@ package body Sem_Util is
       else
          case Nkind (N) is
             when N_Selected_Component =>
-               return Is_SPARK_Object_Reference (Prefix (N));
+               return Is_SPARK_05_Object_Reference (Prefix (N));
 
             when others =>
                return False;
          end case;
       end if;
-   end Is_SPARK_Object_Reference;
+   end Is_SPARK_05_Object_Reference;
 
    ------------------
    -- Is_Statement --
@@ -15116,7 +15117,8 @@ package body Sem_Util is
            and then (Typ = 't' or else Ekind (Ent) = E_Package)
          then
             Error_Msg_Node_1 := Endl;
-            Check_SPARK_Restriction ("`END &` required", Endl, Force => True);
+            Check_SPARK_05_Restriction
+              ("`END &` required", Endl, Force => True);
          end if;
       end if;
 
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index b322405..cdb84dc 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1312,14 +1312,16 @@ package Sem_Util is
    --  represent use of the N_Identifier node for a true identifier, when
    --  normally such nodes represent a direct name.
 
-   function Is_SPARK_Initialization_Expr (N : Node_Id) return Boolean;
+   function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean;
    --  Determines if the tree referenced by N represents an initialization
-   --  expression in SPARK, suitable for initializing an object in an object
-   --  declaration.
-
-   function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
-   --  Determines if the tree referenced by N represents an object in SPARK.
-   --  This differs from Is_Object_Reference in that ???
+   --  expression in SPARK 2005, suitable for initializing an object in an
+   --  object declaration.
+
+   function Is_SPARK_05_Object_Reference (N : Node_Id) return Boolean;
+   --  Determines if the tree referenced by N represents an object in SPARK
+   --  2005. This differs from Is_Object_Reference in that only variables,
+   --  constants, formal parameters, and selected_components of those are
+   --  valid objects in SPARK 2005.
 
    function Is_Statement (N : Node_Id) return Boolean;
    pragma Inline (Is_Statement);