aspects.adb, [...]: Remove all entries for Refined_Pre from the various tables.

2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb, aspects.ads, sem_prag.ads: Remove all entries
	for Refined_Pre from the various tables.
	* par-prag.adb: Remove the entry for Refined_Pre from the list
	of pragmas not needing special processing by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications):
	Remove the processing for aspect Refined_Pre.
	(Check_Aspect_At_Freeze_Point): Remove the entry for aspect
	Refined_Pre.
	* sem_prag.adb (Analyze_Pragma): Refined_Pre is no longer a
	valid assertion kind. Remove the analysis of pragma Refined_Pre.
	(Analyze_Refined_Pragma): Update the comment on usage.
	(Find_Related_Subprogram_Or_Body): Update the comment on
	usage. Pragma Refined_Pre is no longer processed by this routine.
	(Is_Valid_Assertion_Kind): Refined_Pre is no longer a valid
	assertion kind.
	* snames.ads-tmpl: Remove predefined name Refined_Pre. Remove
	the pragma id for Refined_Pre.

From-SVN: r203765

gcc/ada/ChangeLog

 2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* aspects.adb, aspects.ads, sem_prag.ads: Remove all entries
+	for Refined_Pre from the various tables.
+	* par-prag.adb: Remove the entry for Refined_Pre from the list
+	of pragmas not needing special processing by the parser.
+	* sem_ch13.adb (Analyze_Aspect_Specifications):
+	Remove the processing for aspect Refined_Pre.
+	(Check_Aspect_At_Freeze_Point): Remove the entry for aspect
+	Refined_Pre.
+	* sem_prag.adb (Analyze_Pragma): Refined_Pre is no longer a
+	valid assertion kind. Remove the analysis of pragma Refined_Pre.
+	(Analyze_Refined_Pragma): Update the comment on usage.
+	(Find_Related_Subprogram_Or_Body): Update the comment on
+	usage. Pragma Refined_Pre is no longer processed by this routine.
+	(Is_Valid_Assertion_Kind): Refined_Pre is no longer a valid
+	assertion kind.
+	* snames.ads-tmpl: Remove predefined name Refined_Pre. Remove
+	the pragma id for Refined_Pre.
+
+2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* exp_util.adb, exp_util.ads (Entity_Of): Moved to Sem_Util.
 	* sem_prag.adb (Analyze_Global_In_Decl_List): Mark a null
 	item list as being analyzed.

gcc/ada/aspects.adb

@@ -471,7 +471,6 @@ package body Aspects is
     Aspect_Refined_Depends              => Aspect_Refined_Depends,
     Aspect_Refined_Global               => Aspect_Refined_Global,
     Aspect_Refined_Post                 => Aspect_Refined_Post,
-    Aspect_Refined_Pre                  => Aspect_Refined_Pre,
     Aspect_Refined_State                => Aspect_Refined_State,
     Aspect_Remote_Access_Type           => Aspect_Remote_Access_Type,
     Aspect_Remote_Call_Interface        => Aspect_Remote_Call_Interface,

gcc/ada/aspects.ads

@@ -116,7 +116,6 @@ package Aspects is
       Aspect_Refined_Depends,               -- GNAT
       Aspect_Refined_Global,                -- GNAT
       Aspect_Refined_Post,                  -- GNAT
-      Aspect_Refined_Pre,                   -- GNAT
       Aspect_Refined_State,                 -- GNAT
       Aspect_Relative_Deadline,
       Aspect_Scalar_Storage_Order,          -- GNAT
@@ -331,7 +330,6 @@ package Aspects is
       Aspect_Refined_Depends         => Expression,
       Aspect_Refined_Global          => Expression,
       Aspect_Refined_Post            => Expression,
-      Aspect_Refined_Pre             => Expression,
       Aspect_Refined_State           => Expression,
       Aspect_Relative_Deadline       => Expression,
       Aspect_Scalar_Storage_Order    => Expression,
@@ -434,7 +432,6 @@ package Aspects is
       Aspect_Refined_Depends              => Name_Refined_Depends,
       Aspect_Refined_Global               => Name_Refined_Global,
       Aspect_Refined_Post                 => Name_Refined_Post,
-      Aspect_Refined_Pre                  => Name_Refined_Pre,
       Aspect_Refined_State                => Name_Refined_State,
       Aspect_Relative_Deadline            => Name_Relative_Deadline,
       Aspect_Remote_Access_Type           => Name_Remote_Access_Type,
@@ -663,7 +660,6 @@ package Aspects is
       Aspect_Dimension                    => Never_Delay,
       Aspect_Dimension_System             => Never_Delay,
       Aspect_Refined_Post                 => Never_Delay,
-      Aspect_Refined_Pre                  => Never_Delay,
       Aspect_SPARK_Mode                   => Never_Delay,
       Aspect_Synchronization              => Never_Delay,
       Aspect_Test_Case                    => Never_Delay,
@@ -726,7 +722,6 @@ package Aspects is
      (Aspect_Refined_Depends              => True,
       Aspect_Refined_Global               => True,
       Aspect_Refined_Post                 => True,
-      Aspect_Refined_Pre                  => True,
       Aspect_SPARK_Mode                   => True,
       Aspect_Warnings                     => True,
       others                              => False);

gcc/ada/par-prag.adb

@@ -1259,7 +1259,6 @@ begin
            Pragma_Refined_Depends                |
            Pragma_Refined_Global                 |
            Pragma_Refined_Post                   |
-           Pragma_Refined_Pre                    |
            Pragma_Refined_State                  |
            Pragma_Relative_Deadline              |
            Pragma_Remote_Access_Type             |

gcc/ada/sem_ch13.adb

@@ -2184,15 +2184,6 @@ package body Sem_Ch13 is
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Name_Refined_Post);
 
-               --  Refined_Pre
-
-               --  Disable the support for aspect Refined_Pre as its static and
-               --  runtime semantics are still under heavy design.
-
-               when Aspect_Refined_Pre =>
-                  Error_Msg_NE ("aspect & is not supported", Aspect, Id);
-                  goto Continue;
-
                --  Refined_State
 
                when Aspect_Refined_State => Refined_State : declare
@@ -7907,7 +7898,6 @@ package body Sem_Ch13 is
               Aspect_Refined_Depends      |
               Aspect_Refined_Global       |
               Aspect_Refined_Post         |
-              Aspect_Refined_Pre          |
               Aspect_Refined_State        |
               Aspect_SPARK_Mode           |
               Aspect_Test_Case            =>

gcc/ada/sem_prag.adb

@@ -236,17 +236,17 @@ package body Sem_Prag is
      (Prag      : Node_Id;
       Do_Checks : Boolean := False) return Node_Id;
    --  Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global,
-   --  Refined_Depends, Refined_Global, Refined_Post and Refined_Pre. Find the
-   --  declaration of the related subprogram [body or stub] subject to pragma
-   --  Prag. If flag Do_Checks is set, the routine reports duplicate pragmas
-   --  and detects improper use of refinement pragmas in stand alone expression
-   --  functions. The returned value depends on the related pragma as follows:
+   --  Refined_Depends, Refined_Global and Refined_Post. Find the declaration
+   --  of the related subprogram [body or stub] subject to pragma Prag. If flag
+   --  Do_Checks is set, the routine reports duplicate pragmas and detects
+   --  improper use of refinement pragmas in stand alone expression functions.
+   --  The returned value depends on the related pragma as follows:
    --    1) Pragmas Contract_Cases, Depends and Global yield the corresponding
    --       N_Subprogram_Declaration node or if the pragma applies to a stand
    --       alone body, the N_Subprogram_Body node or Empty if illegal.
-   --    2) Pragmas Refined_Depends, Refined_Global, Refined_Post and
-   --       Refined_Pre yield N_Subprogram_Body or N_Subprogram_Body_Stub nodes
-   --       or Empty if illegal.
+   --    2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield
+   --       N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if
+   --       illegal.
 
    function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
    --  If Def_Id refers to a renamed subprogram, then the base subprogram (the
@@ -2573,8 +2573,8 @@ package body Sem_Prag is
          Body_Id : out Entity_Id;
          Legal   : out Boolean);
       --  Subsidiary routine to the analysis of body pragmas Refined_Depends,
-      --  Refined_Global, Refined_Post and Refined_Pre. Check the placement and
-      --  related context of the pragma. Spec_Id is the entity of the related
+      --  Refined_Global and Refined_Post. Check the placement and related
+      --  context of the pragma. Spec_Id is the entity of the related
       --  subprogram. Body_Id is the entity of the subprogram body. Flag Legal
       --  is set when the pragma is properly placed.
 
@@ -9967,7 +9967,6 @@ package body Sem_Prag is
          --                        Precondition         |
          --                        Predicate            |
          --                        Refined_Post         |
-         --                        Refined_Pre          |
          --                        Statement_Assertions
 
          --  Note: The RM_ASSERTION_KIND list is language-defined, and the
@@ -17204,29 +17203,18 @@ package body Sem_Prag is
             end if;
          end Refined_Depends_Global;
 
-         ------------------------------
-         -- Refined_Post/Refined_Pre --
-         ------------------------------
+         ------------------
+         -- Refined_Post --
+         ------------------
 
          --  pragma Refined_Post (boolean_EXPRESSION);
-         --  pragma Refined_Pre  (boolean_EXPRESSION);
 
-         when Pragma_Refined_Post |
-              Pragma_Refined_Pre  => Refined_Pre_Post :
-         declare
+         when Pragma_Refined_Post => Refined_Post : declare
             Body_Id : Entity_Id;
             Legal   : Boolean;
             Spec_Id : Entity_Id;
 
          begin
-            --  Disable the support for pragma Refined_Pre as its static and
-            --  runtime semantics are still under heavy design. The pragma is
-            --  silently ignored.
-
-            if Pname = Name_Refined_Pre then
-               Set_Is_Ignored (N);
-            end if;
-
             Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
 
             --  Analyze the boolean expression as a "spec expression"
@@ -17234,7 +17222,7 @@ package body Sem_Prag is
             if Legal then
                Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id);
             end if;
-         end Refined_Pre_Post;
+         end Refined_Post;
 
          -------------------
          -- Refined_State --
@@ -22448,8 +22436,7 @@ package body Sem_Prag is
       Look_For_Body : constant Boolean :=
                         Nam_In (Nam, Name_Refined_Depends,
                                      Name_Refined_Global,
-                                     Name_Refined_Post,
-                                     Name_Refined_Pre);
+                                     Name_Refined_Post);
       --  Refinement pragmas must be associated with a subprogram body [stub]
 
    begin
@@ -22877,7 +22864,6 @@ package body Sem_Prag is
       Pragma_Refined_Depends                => -1,
       Pragma_Refined_Global                 => -1,
       Pragma_Refined_Post                   => -1,
-      Pragma_Refined_Pre                    => -1,
       Pragma_Refined_State                  => -1,
       Pragma_Relative_Deadline              => -1,
       Pragma_Remote_Access_Type             => -1,
@@ -23202,7 +23188,6 @@ package body Sem_Prag is
             Name_Precondition         |
             Name_Predicate            |
             Name_Refined_Post         |
-            Name_Refined_Pre          |
             Name_Statement_Assertions => return True;
 
          when others                  => return False;

gcc/ada/sem_prag.ads

@@ -41,7 +41,6 @@ package Sem_Prag is
      (Pragma_Refined_Depends => True,
       Pragma_Refined_Global  => True,
       Pragma_Refined_Post    => True,
-      Pragma_Refined_Pre     => True,
       Pragma_SPARK_Mode      => True,
       Pragma_Warnings        => True,
       others                 => False);

gcc/ada/snames.ads-tmpl

@@ -586,7 +586,6 @@ package Snames is
    Name_Refined_Depends                : constant Name_Id := N + $; -- GNAT
    Name_Refined_Global                 : constant Name_Id := N + $; -- GNAT
    Name_Refined_Post                   : constant Name_Id := N + $; -- GNAT
-   Name_Refined_Pre                    : constant Name_Id := N + $; -- GNAT
    Name_Refined_State                  : constant Name_Id := N + $; -- GNAT
    Name_Relative_Deadline              : constant Name_Id := N + $; -- Ada 05
    Name_Remote_Access_Type             : constant Name_Id := N + $; -- GNAT
@@ -1882,7 +1881,6 @@ package Snames is
       Pragma_Refined_Depends,
       Pragma_Refined_Global,
       Pragma_Refined_Post,
-      Pragma_Refined_Pre,
       Pragma_Refined_State,
       Pragma_Relative_Deadline,
       Pragma_Remote_Access_Type,