[multiple changes]

2013-07-08  Gary Dismukes  <dismukes@adacore.com>

	* freeze.adb: Minor typo fixes.

2013-07-08  Robert Dewar  <dewar@adacore.com>

	* gnat_rm.texi: Document SPARK_05 (replaces SPARK) Document
	obsolete recognition of SPARK Document all other obsolete synonyms
	for old restrictions.
	* restrict.adb (Check_SPARK_Restriction): SPARK_05 replaces
	SPARK (Process_Restriction_Synonyms): Handle SPARK as synonym
	for SPARK_05.
	* restrict.ads: Restriction SPARK_05 replaces SPARK.
	* s-rident.ads: Replace restriction SPARK by SPARK_05 Add SPARK
	as synonym for SPARK_05.
	* sem_prag.adb: Minor reformatting.
	* snames.ads-tmpl: Add entries for Name_SPARK and Name_SPARK_05.

From-SVN: r200763

gcc/ada/ChangeLog

+2013-07-08  Gary Dismukes  <dismukes@adacore.com>
+
+	* freeze.adb: Minor typo fixes.
+
+2013-07-08  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Document SPARK_05 (replaces SPARK) Document
+	obsolete recognition of SPARK Document all other obsolete synonyms
+	for old restrictions.
+	* restrict.adb (Check_SPARK_Restriction): SPARK_05 replaces
+	SPARK (Process_Restriction_Synonyms): Handle SPARK as synonym
+	for SPARK_05.
+	* restrict.ads: Restriction SPARK_05 replaces SPARK.
+	* s-rident.ads: Replace restriction SPARK by SPARK_05 Add SPARK
+	as synonym for SPARK_05.
+	* sem_prag.adb: Minor reformatting.
+	* snames.ads-tmpl: Add entries for Name_SPARK and Name_SPARK_05.
+
 2013-07-08  Robert Dewar  <dewar@adacore.com>
 
 	* sem_dim.adb: Minor error message change.

gcc/ada/freeze.adb

@@ -3415,15 +3415,16 @@ package body Freeze is
             --  a size given for an array where the array needs to be packed,
             --  but was not so the size cannot be honored. This is the case
             --  where implicit packing may apply. The reason we do this so
-            --  early is that if we have implicit packing, the lagout of the
+            --  early is that if we have implicit packing, the layout of the
             --  base type is affected, so we must do this before we freeze
             --  the base type.
 
             --  We could do this processing only if implicit packing is enabled
             --  since in all other cases, the error would be caught by the back
             --  end. However, we choose to do the check even if we do not have
-            --  implicit packingh enabled, since this allows us to give a more
-            --  useful error message (advising the use of pack or the pragma).
+            --  implicit packing enabled, since this allows us to give a more
+            --  useful error message (advising use of pragmas Implicit_Packing
+            --  or Pack).
 
             if Is_Array_Type (E) then
                declare

gcc/ada/gnat_rm.texi

@@ -454,7 +454,7 @@ Program Unit Level Restrictions
 * No_Implicit_Aliasing::
 * No_Obsolescent_Features::
 * No_Wide_Characters::
-* SPARK::
+* SPARK_05::
 
 The Implementation of Standard I/O
 
@@ -8951,6 +8951,12 @@ Note that this restriction is checked at run time. Violation of this
 restriction results in the raising of Program_Error exception at the point of
 the call.
 
+@findex Max_Entry_Queue_Depth
+The restriction @code{Max_Entry_Queue_Depth} is recognized as a
+synonym for @code{Max_Entry_Queue_Length}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
 @node Max_Protected_Entries
 @unnumberedsubsec Max_Protected_Entries
 @findex Max_Protected_Entries
@@ -9137,6 +9143,12 @@ operations defined in package Ada.Interrupts
 (Is_Reserved, Is_Attached, Current_Handler, Attach_Handler, Exchange_Handler,
 Detach_Handler, and Reference).
 
+@findex No_Dynamic_Interrupts
+The restriction @code{No_Dynamic_Interrupts} is recognized as a
+synonym for @code{No_Dynamic_Attachment}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
 @node No_Dynamic_Priorities
 @unnumberedsubsec No_Dynamic_Priorities
 @findex No_Dynamic_Priorities
@@ -9378,6 +9390,12 @@ appearing in source code.
 are permitted and prevents keyword @code{requeue} from being used in source
 code.
 
+@findex No_Requeue
+The restriction @code{No_Requeue} is recognized as a
+synonym for @code{No_Requeue_Statements}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on oNobsolescent features are activated).
+
 @node No_Secondary_Stack
 @unnumberedsubsec No_Secondary_Stack
 @findex No_Secondary_Stack
@@ -9459,6 +9477,12 @@ or types containing task subcomponents.
 [GNAT] This restriction ensures at compile time that there are no implicit or
 explicit dependencies on the package @code{Ada.Task_Attributes}.
 
+@findex No_Task_Attributes
+The restriction @code{No_Task_Attributes} is recognized as a synonym
+for @code{No_Task_Attributes_Package}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
 @node No_Task_Hierarchy
 @unnumberedsubsec No_Task_Hierarchy
 @findex No_Task_Hierarchy
@@ -9498,6 +9522,12 @@ declarations for protected types are restricted to either static boolean
 expressions or references to simple boolean variables defined in the private
 part of the protected type.  No other form of entry barriers is permitted.
 
+@findex Boolean_Entry_Barriers
+The restriction @code{Boolean_Entry_Barriers} is recognized as a
+synonym for @code{Simple_Barriers}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
 @node Static_Priorities
 @unnumberedsubsec Static_Priorities
 @findex Static_Priorities
@@ -9533,7 +9563,7 @@ other compilation units in the partition.
 * No_Implicit_Aliasing::
 * No_Obsolescent_Features::
 * No_Wide_Characters::
-* SPARK::
+* SPARK_05::
 @end menu
 
 @node No_Elaboration_Code
@@ -9663,13 +9693,19 @@ appear, and that no wide or wide wide string or character literals
 appear in the program (that is literals representing characters not in
 type @code{Character}).
 
-@node SPARK
-@unnumberedsubsec SPARK
-@findex SPARK
+@node SPARK_05
+@unnumberedsubsec SPARK_05
+@findex SPARK_05
 [GNAT] This restriction checks at compile time that some constructs
 forbidden in SPARK 2005 are not present. Error messages related to
 SPARK restriction have the form:
 
+@findex SPARK
+The restriction @code{SPARK} is recognized as a
+synonym for @code{SPARK_05}. This is retained for historical
+compatibility purposes (and an unconditional warning will be generated
+for its use, advising replacement by @code{SPARK}.
+
 @smallexample
 violation of restriction "SPARK" at <file>
  <error message>

gcc/ada/restrict.adb

@@ -166,7 +166,7 @@ package body Restrict is
    begin
       if Force or else Comes_From_Source (Original_Node (N)) then
 
-         if Restriction_Check_Required (SPARK)
+         if Restriction_Check_Required (SPARK_05)
            and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
          then
             return;
@@ -177,7 +177,7 @@ package body Restrict is
          --  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));
+         Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
          Error_Msg_Sloc := Save_Error_Msg_Sloc;
 
          if Msg_Issued then
@@ -194,7 +194,7 @@ package body Restrict is
 
       if Comes_From_Source (Original_Node (N)) then
 
-         if Restriction_Check_Required (SPARK)
+         if Restriction_Check_Required (SPARK_05)
            and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
          then
             return;
@@ -205,7 +205,7 @@ package body Restrict is
          --  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));
+         Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
          Error_Msg_Sloc := Save_Error_Msg_Sloc;
 
          if Msg_Issued then
@@ -880,10 +880,22 @@ package body Restrict is
          when Name_No_Task_Attributes =>
             New_Name := Name_No_Task_Attributes_Package;
 
+         --  SPARK is special in that we unconditionally warn
+
+         when Name_SPARK =>
+            Error_Msg_Name_1 := Name_SPARK;
+            Error_Msg_N ("restriction identifier % is obsolescent??", N);
+            Error_Msg_Name_1 := Name_SPARK_05;
+            Error_Msg_N ("|use restriction identifier % instead??", N);
+            return Name_SPARK_05;
+
          when others =>
             return Old_Name;
       end case;
 
+      --  Output warning if we are warning on obsolescent features for all
+      --  cases other than SPARK.
+
       if Warn_On_Obsolescent_Feature then
          Error_Msg_Name_1 := Old_Name;
          Error_Msg_N ("restriction identifier % is obsolescent?j?", N);
@@ -983,10 +995,10 @@ package body Restrict is
 
       procedure Id_Case (S : String; Quotes : Boolean := True);
       --  Given a string S, case it according to current identifier casing,
-      --  except for SPARK (an acronym) which is set all upper case, and store
-      --  in Error_Msg_String. Then append `~` to the message buffer to output
-      --  the string unchanged surrounded in quotes. The quotes are suppressed
-      --  if Quotes = False.
+      --  except for SPARK_05 (an acronym) which is set all upper case, and
+      --  store in Error_Msg_String. Then append `~` to the message buffer
+      --  to output the string unchanged surrounded in quotes. The quotes
+      --  are suppressed if Quotes = False.
 
       --------------
       -- Add_Char --
@@ -1017,7 +1029,7 @@ package body Restrict is
          Name_Buffer (1 .. S'Last) := S;
          Name_Len := S'Length;
 
-         if R = SPARK then
+         if R = SPARK_05 then
             Set_All_Upper_Case;
          else
             Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N))));

gcc/ada/restrict.ads

@@ -142,7 +142,7 @@ package Restrict is
       No_Wide_Characters                 => True,
       Static_Priorities                  => True,
       Static_Storage_Size                => True,
-      SPARK                              => True,
+      SPARK_05                           => True,
       others                             => False);
 
    --  The following table records entries made by Restrictions pragmas
@@ -180,7 +180,7 @@ package Restrict is
    -- SPARK Restriction Control --
    -------------------------------
 
-   --  SPARK HIDE directives allow the effect of the SPARK restriction to be
+   --  SPARK HIDE directives allow the effect of the SPARK_05 restriction to be
    --  turned off for a specified region of code, and the following tables are
    --  the data structures used to keep track of these regions.
 
@@ -282,10 +282,10 @@ package Restrict is
      (Msg   : String;
       N     : Node_Id;
       Force : Boolean := False);
-   --  Node N represents a construct not allowed in formal mode. If this is a
-   --  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.
+   --  Node N represents a construct not allowed in formal mode. If this is
+   --  a source node, or if the restriction is forced (Force = True), and
+   --  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

gcc/ada/s-rident.ads

@@ -175,7 +175,7 @@ package System.Rident is
       No_Elaboration_Code,                       -- GNAT
       No_Obsolescent_Features,                   -- Ada 2005 AI-368
       No_Wide_Characters,                        -- GNAT
-      SPARK,                                     -- GNAT
+      SPARK_05,                                  -- GNAT
 
       --  The following cases require a parameter value
 
@@ -223,13 +223,14 @@ package System.Rident is
    No_Dynamic_Interrupts  : Restriction_Id renames No_Dynamic_Attachment;
    No_Requeue             : Restriction_Id renames No_Requeue_Statements;
    No_Task_Attributes     : Restriction_Id renames No_Task_Attributes_Package;
+   SPARK                  : Restriction_Id renames SPARK_05;
 
    subtype All_Restrictions is Restriction_Id range
      Simple_Barriers .. Max_Storage_At_Blocking;
    --  All restrictions (excluding only Not_A_Restriction_Id)
 
    subtype All_Boolean_Restrictions is Restriction_Id range
-     Simple_Barriers .. SPARK;
+     Simple_Barriers .. SPARK_05;
    --  All restrictions which do not take a parameter
 
    subtype Partition_Boolean_Restrictions is All_Boolean_Restrictions range
@@ -240,7 +241,7 @@ package System.Rident is
    --  case of Boolean restrictions.
 
    subtype Cunit_Boolean_Restrictions is All_Boolean_Restrictions range
-     Immediate_Reclamation .. SPARK;
+     Immediate_Reclamation .. SPARK_05;
    --  Boolean restrictions that are not checked for partition consistency
    --  and that thus apply only to the current unit. Note that for these
    --  restrictions, the compiler does not apply restrictions found in

gcc/ada/sem_prag.adb

@@ -7016,7 +7016,7 @@ package body Sem_Prag is
       --  Start of processing for Process_Restrictions_Or_Restriction_Warnings
 
       begin
-         --  Ignore all Restrictions pragma in CodePeer mode
+         --  Ignore all Restrictions pragmas in CodePeer mode
 
          if CodePeer_Mode then
             return;

gcc/ada/snames.ads-tmpl

@@ -762,6 +762,8 @@ package Snames is
    Name_Semaphore                      : constant Name_Id := N + $;
    Name_Short_Descriptor               : constant Name_Id := N + $;
    Name_Simple_Barriers                : constant Name_Id := N + $;
+   Name_SPARK                          : constant Name_Id := N + $;
+   Name_SPARK_05                       : constant Name_Id := N + $;
    Name_Spec_File_Name                 : constant Name_Id := N + $;
    Name_State                          : constant Name_Id := N + $;
    Name_Statement_Assertions           : constant Name_Id := N + $;