2013-10-13 Robert Dewar <dewar@adacore.com>

	* gnat_rm.texi: Add documentation for pragmas Pre[_Class]
	Post[_Class].
	* par-ch2.adb (Skip_Pragma_Semicolon): Handle extra semicolon nicely.
	* par-prag.adb: Add entries for pragmas Pre[_Class] and
	Post[_Class].
	* sem_prag.adb: Add handling of pragmas Pre[_Class] and
	Post[_Class].
	* sem_util.adb (Original_Aspect_Name): Moved here from
	Sem_Prag.Original_Name, and modified to handle pragmas
	Pre/Post/Pre_Class/Post_Class.
	* sem_util.ads (Original_Aspect_Name): Moved here from
	Sem_Prag.Original_Name.
	* snames.ads-tmpl: Add entries for pragmas Pre[_Class] and
	Post[_Class].

2013-10-13  Robert Dewar  <dewar@adacore.com>

	* einfo.adb, sem_ch6.adb: Minor reformatting.



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

10 files changed, 496 insertions, 112 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 65093fa655c..0b09903605f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,24 @@
+2013-10-13  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Add documentation for pragmas Pre[_Class]
+	Post[_Class].
+	* par-ch2.adb (Skip_Pragma_Semicolon): Handle extra semicolon nicely.
+	* par-prag.adb: Add entries for pragmas Pre[_Class] and
+	Post[_Class].
+	* sem_prag.adb: Add handling of pragmas Pre[_Class] and
+	Post[_Class].
+	* sem_util.adb (Original_Aspect_Name): Moved here from
+	Sem_Prag.Original_Name, and modified to handle pragmas
+	Pre/Post/Pre_Class/Post_Class.
+	* sem_util.ads (Original_Aspect_Name): Moved here from
+	Sem_Prag.Original_Name.
+	* snames.ads-tmpl: Add entries for pragmas Pre[_Class] and
+	Post[_Class].
+
+2013-10-13  Robert Dewar  <dewar@adacore.com>
+
+	* einfo.adb, sem_ch6.adb: Minor reformatting.
+
 2013-10-13  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* einfo.adb: Add node/list usage for Refined_State
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index e9c262afaac..fa0daa98ce6 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -6292,16 +6292,18 @@ package body Einfo is
    ----------------
 
    function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
-      Is_CDG       : constant Boolean :=
-                       Id = Pragma_Depends
-                         or else Id = Pragma_Global
-                         or else Id = Pragma_Refined_Depends
-                         or else Id = Pragma_Refined_Global;
-      Is_CTC      : constant Boolean :=
-                      Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case;
-      Is_PPC      : constant Boolean :=
-                      Id = Pragma_Precondition
-                        or else Id = Pragma_Postcondition;
+      Is_CDG  : constant Boolean :=
+                  Id = Pragma_Depends         or else
+                  Id = Pragma_Global          or else
+                  Id = Pragma_Refined_Depends or else
+                  Id = Pragma_Refined_Global;
+      Is_CTC : constant Boolean :=
+                  Id = Pragma_Contract_Cases  or else
+                  Id = Pragma_Test_Case;
+      Is_PPC : constant Boolean :=
+                  Id = Pragma_Precondition     or else
+                  Id = Pragma_Postcondition;
+
       In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
 
       Item   : Node_Id;
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index cd518647e40..833922e4650 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -206,11 +206,15 @@ Implementation Defined Pragmas
 * Pragma Passive::
 * Pragma Persistent_BSS::
 * Pragma Polling::
+* Pragma Post::
 * Pragma Postcondition::
+* Pragma Post_Class::
+* Pragma Pre::
 * Pragma Precondition::
 * Pragma Predicate::
 * Pragma Preelaborable_Initialization::
 * Pragma Preelaborate_05::
+* Pragma Pre_Class::
 * Pragma Priority_Specific_Dispatching::
 * Pragma Profile::
 * Pragma Profile_Warnings::
@@ -1022,11 +1026,15 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Passive::
 * Pragma Persistent_BSS::
 * Pragma Polling::
+* Pragma Post::
 * Pragma Postcondition::
+* Pragma Post_Class::
+* Pragma Pre::
 * Pragma Precondition::
 * Pragma Predicate::
 * Pragma Preelaborable_Initialization::
 * Pragma Preelaborate_05::
+* Pragma Pre_Class::
 * Pragma Priority_Specific_Dispatching::
 * Pragma Profile::
 * Pragma Profile_Warnings::
@@ -1393,7 +1401,10 @@ are implementation defined additions recognized by the GNAT compiler.
 The pragma applies in both cases to pragmas and aspects with matching
 names, e.g. @code{Pre} applies to the Pre aspect, and @code{Precondition}
 applies to both the @code{Precondition} pragma
-and the aspect @code{Precondition}.
+and the aspect @code{Precondition}. Note that the identifiers for
+pragmas Pre_Class and Post_Class are Pre'Class and Post'Class (not
+Pre_Class and Post_Class), since these pragmas are intended to be
+identical to the corresponding aspects).
 
 If the policy is @code{CHECK}, then assertions are enabled, i.e.
 the corresponding pragma or aspect is activated.
@@ -5016,6 +5027,28 @@ Note that polling can also be enabled by use of the @option{-gnatP} switch.
 @xref{Switches for gcc,,, gnat_ugn, @value{EDITION} User's Guide}, for
 details.
 
+@node Pragma Post
+@unnumberedsec Pragma Post
+@cindex Post
+@cindex Checks, postconditions
+@findex Postconditions
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Post (Boolean_Expression);
+@end smallexample
+
+@noindent
+The @code{Post} pragma is intended to be an exact replacement for
+the language-defined
+@code{Post} aspect, and shares its restrictions and semantics.
+It must appear either immediately following the corresponding
+subprogram declaration (only other pragmas may intervene), or
+if there is no separate subprogram declaration, then it can
+appear at the start of the declarations in a subprogram body
+(preceded only by other pragmas).
+
 @node Pragma Postcondition
 @unnumberedsec Pragma Postcondition
 @cindex Postcondition
@@ -5173,6 +5206,69 @@ inlining (-gnatN option set) are accepted and legality-checked
 by the compiler, but are ignored at run-time even if postcondition
 checking is enabled.
 
+Note that pragma @code{Postcondition} differs from the language-defined
+@code{Post} aspect (and corresponding @code{Post} pragma) in allowing
+multiple occurrences, allowing occurences in the body even if there
+is a separate spec, and allowing a second string parameter, and the
+use of the pragma identifier @code{Check}. Historically, pragma
+@code{Postcondition} was implemented prior to the development of
+Ada 2012, and has been retained in its original form for
+compatibility purposes.
+
+@node Pragma Post_Class
+@unnumberedsec Pragma Post_Class
+@cindex Post
+@cindex Checks, postconditions
+@findex Postconditions
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Post_Class (Boolean_Expression);
+@end smallexample
+
+@noindent
+The @code{Post_Class} pragma is intended to be an exact replacement for
+the language-defined
+@code{Post'Class} aspect, and shares its restrictions and semantics.
+It must appear either immediately following the corresponding
+subprogram declaration (only other pragmas may intervene), or
+if there is no separate subprogram declaration, then it can
+appear at the start of the declarations in a subprogram body
+(preceded only by other pragmas).
+
+Note: This pragma is called @code{Post_Class} rather than
+@code{Post'Class} because the latter would not be strictly
+conforming to the allowed syntax for pragmas. The motivation
+for provinding pragmas equivalent to the aspects is to allow a program
+to be written using the pragmas, and then compiled if necessary
+using an Ada compiler that does not recognize the pragmas or
+aspects, but is prepared to ignore the pragmas. The assertion
+policy that controls this pragma is @code{Post'Class}, not
+@code{Post_Class}.
+
+@node Pragma Pre
+@unnumberedsec Pragma Pre
+@cindex Pre
+@cindex Checks, preconditions
+@findex Preconditions
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Pre (Boolean_Expression);
+@end smallexample
+
+@noindent
+The @code{Pre} pragma is intended to be an exact replacement for
+the language-defined
+@code{Pre} aspect, and shares its restrictions and semantics.
+It must appear either immediately following the corresponding
+subprogram declaration (only other pragmas may intervene), or
+if there is no separate subprogram declaration, then it can
+appear at the start of the declarations in a subprogram body
+(preceded only by other pragmas).
+
 @node Pragma Precondition
 @unnumberedsec Pragma Precondition
 @cindex Preconditions
@@ -5221,6 +5317,15 @@ inlining (-gnatN option set) are accepted and legality-checked
 by the compiler, but are ignored at run-time even if precondition
 checking is enabled.
 
+Note that pragma @code{Precondition} differs from the language-defined
+@code{Pre} aspect (and corresponding @code{Pre} pragma) in allowing
+multiple occurrences, allowing occurences in the body even if there
+is a separate spec, and allowing a second string parameter, and the
+use of the pragma identifier @code{Check}. Historically, pragma
+@code{Precondition} was implemented prior to the development of
+Ada 2012, and has been retained in its original form for
+compatibility purposes.
+
 @node Pragma Predicate
 @unnumberedsec Pragma Predicate
 @findex Predicate
@@ -5295,6 +5400,38 @@ equivalent to @code{pragma Prelaborate} when operating in later
 Ada versions. This is used to handle some cases where packages
 not previously preelaborable became so in Ada 2005.
 
+@node Pragma Pre_Class
+@unnumberedsec Pragma Pre_Class
+@cindex Pre_Class
+@cindex Checks, preconditions
+@findex Preconditions
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Pre_Class (Boolean_Expression);
+@end smallexample
+
+@noindent
+The @code{Pre_Class} pragma is intended to be an exact replacement for
+the language-defined
+@code{Pre'Class} aspect, and shares its restrictions and semantics.
+It must appear either immediately following the corresponding
+subprogram declaration (only other pragmas may intervene), or
+if there is no separate subprogram declaration, then it can
+appear at the start of the declarations in a subprogram body
+(preceded only by other pragmas).
+
+Note: This pragma is called @code{Pre_Class} rather than
+@code{Pre'Class} because the latter would not be strictly
+conforming to the allowed syntax for pragmas. The motivation
+for providing pragmas equivalent to the aspects is to allow a program
+to be written using the pragmas, and then compiled if necessary
+using an Ada compiler that does not recognize the pragmas or
+aspects, but is prepared to ignore the pragmas. The assertion
+policy that controls this pragma is @code{Pre'Class}, not
+@code{Pre_Class}.
+
 @node Pragma Priority_Specific_Dispatching
 @unnumberedsec Pragma Priority_Specific_Dispatching
 @findex Priority_Specific_Dispatching
diff --git a/gcc/ada/par-ch2.adb b/gcc/ada/par-ch2.adb
index 224c63b7eb9..2218dacb17e 100644
--- a/gcc/ada/par-ch2.adb
+++ b/gcc/ada/par-ch2.adb
@@ -250,23 +250,15 @@ package body Ch2 is
 
       procedure Skip_Pragma_Semicolon is
       begin
-         if Token /= Tok_Semicolon then
+         --  If skipping the pragma, ignore a missing semicolon
 
-            --  If skipping the pragma, ignore a missing semicolon
+         if Token /= Tok_Semicolon and then Skipping then
+            null;
 
-            if Skipping then
-               null;
-
-            --  Otherwise demand a semicolon
-
-            else
-               T_Semicolon;
-            end if;
-
-         --  Scan past semicolon if present
+         --  Otherwise demand a semicolon
 
          else
-            Scan;
+            T_Semicolon;
          end if;
       end Skip_Pragma_Semicolon;
 
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index bf23bc7d609..aed45f96982 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1234,11 +1234,15 @@ begin
            Pragma_Preelaborable_Initialization   |
            Pragma_Polling                        |
            Pragma_Persistent_BSS                 |
+           Pragma_Post                           |
            Pragma_Postcondition                  |
+           Pragma_Post_Class                     |
+           Pragma_Pre                            |
            Pragma_Precondition                   |
            Pragma_Predicate                      |
            Pragma_Preelaborate                   |
            Pragma_Preelaborate_05                |
+           Pragma_Pre_Class                      |
            Pragma_Priority                       |
            Pragma_Priority_Specific_Dispatching  |
            Pragma_Profile                        |
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index aee35fbda3a..acf1aeb812b 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1995,7 +1995,6 @@ package body Sem_Ch6 is
       while Present (Prag) loop
          if Pragma_Name (Prag) = Name_Refined_Depends then
             Analyze_Refined_Depends_In_Decl_Part (Prag);
-
          elsif Pragma_Name (Prag) = Name_Refined_Global then
             Has_Refined_Global := True;
             Analyze_Refined_Global_In_Decl_Part (Prag);
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 4ef1867c112..4fbbfd73cf9 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -236,16 +236,6 @@ package body Sem_Prag is
    --  Get_SPARK_Mode_Id. Convert a name into a corresponding value of type
    --  SPARK_Mode_Id.
 
-   function Original_Name (N : Node_Id) return Name_Id;
-   --  N is a pragma node or aspect specification node. This function returns
-   --  the name of the pragma or aspect in original source form, taking into
-   --  account possible rewrites, and also cases where a pragma comes from an
-   --  aspect (in such cases, the name can be different from the pragma name,
-   --  e.g. a Pre aspect generates a Precondition pragma). This also deals with
-   --  the presence of 'Class, which results in one of the special names
-   --  Name_uPre, Name_uPost, Name_uInvariant, or Name_uType_Invariant being
-   --  returned to represent the corresponding aspects with x'Class names.
-
    procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
    --  Preanalyze the boolean expressions in the Requires and Ensures arguments
    --  of a Test_Case pragma if present (possibly Empty). We treat these as
@@ -1979,6 +1969,13 @@ package body Sem_Prag is
       --  In this version of the procedure, the identifier name is given as
       --  a string with lower case letters.
 
+      procedure Check_Pre_Post;
+      --  Called to perform checks for Pre, Pre_Class, Post, Post_Class
+      --  pragmas. These are processed by transformation to equivalent
+      --  Precondition and Postcondition pragmas, but Pre and Post need an
+      --  additional check that they are not used in a subprogram body when
+      --  there is a separate spec present.
+
       procedure Check_Precondition_Postcondition (In_Body : out Boolean);
       --  Called to process a precondition or postcondition pragma. There are
       --  three cases:
@@ -3392,6 +3389,97 @@ package body Sem_Prag is
          Check_Optional_Identifier (Arg, Name_Find);
       end Check_Optional_Identifier;
 
+      --------------------
+      -- Check_Pre_Post --
+      --------------------
+
+      procedure Check_Pre_Post is
+         P  : Node_Id;
+         PO : Node_Id;
+
+      begin
+         if not Is_List_Member (N) then
+            Pragma_Misplaced;
+         end if;
+
+         --  If we are within an inlined body, the legality of the pragma
+         --  has been checked already.
+
+         if In_Inlined_Body then
+            return;
+         end if;
+
+         --  Search prior declarations
+
+         P := N;
+         while Present (Prev (P)) loop
+            P := Prev (P);
+
+            --  If the previous node is a generic subprogram, do not go to to
+            --  the original node, which is the unanalyzed tree: we need to
+            --  attach the pre/postconditions to the analyzed version at this
+            --  point. They get propagated to the original tree when analyzing
+            --  the corresponding body.
+
+            if Nkind (P) not in N_Generic_Declaration then
+               PO := Original_Node (P);
+            else
+               PO := P;
+            end if;
+
+            --  Skip past prior pragma
+
+            if Nkind (PO) = N_Pragma then
+               null;
+
+            --  Skip stuff not coming from source
+
+            elsif not Comes_From_Source (PO) then
+
+               --  The condition may apply to a subprogram instantiation
+
+               if Nkind (PO) = N_Subprogram_Declaration
+                 and then Present (Generic_Parent (Specification (PO)))
+               then
+                  return;
+
+               elsif Nkind (PO) = N_Subprogram_Declaration
+                 and then In_Instance
+               then
+                  return;
+
+               --  For all other cases of non source code, do nothing
+
+               else
+                  null;
+               end if;
+
+            --  Only remaining possibility is subprogram declaration
+
+            else
+               return;
+            end if;
+         end loop;
+
+         --  If we fall through loop, pragma is at start of list, so see if it
+         --  is at the start of declarations of a subprogram body.
+
+         PO := Parent (N);
+
+         if Nkind (PO) = N_Subprogram_Body
+           and then List_Containing (N) = Declarations (PO)
+         then
+            --  This is only allowed if there is no separate specification
+
+            if Present (Corresponding_Spec (PO)) then
+               Error_Pragma
+                 ("pragma% must apply to subprogram specification");
+            end if;
+
+            return;
+         end if;
+      end Check_Pre_Post;
+
       --------------------------------------
       -- Check_Precondition_Postcondition --
       --------------------------------------
@@ -3431,7 +3519,7 @@ package body Sem_Prag is
             --  compatibility with earlier uses of the Ada pragma, apply this
             --  rule only to aspect specifications.
 
-            --  The above discrpency needs documentation. Robert is dubious
+            --  The above discrepency needs documentation. Robert is dubious
             --  about whether it is a good idea ???
 
             elsif Nkind (PO) = N_Subprogram_Declaration
@@ -4286,7 +4374,7 @@ package body Sem_Prag is
 
             --  Get name from corresponding aspect
 
-            Error_Msg_Name_1 := Original_Name (N);
+            Error_Msg_Name_1 := Original_Aspect_Name (N);
          end if;
       end Fix_Error;
 
@@ -8180,7 +8268,7 @@ package body Sem_Prag is
       --  Here to start processing for recognized pragma
 
       Prag_Id := Get_Pragma_Id (Pname);
-      Pname := Original_Name (N);
+      Pname := Original_Aspect_Name (N);
 
       --  Check applicable policy. We skip this if Is_Checked or Is_Ignored
       --  is already set, indicating that we have already checked the policy
@@ -15056,6 +15144,32 @@ package body Sem_Prag is
             Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
             Polling_Required := (Chars (Get_Pragma_Arg (Arg1)) = Name_On);
 
+         ------------------
+         -- Post[_Class] --
+         ------------------
+
+         --  pragma Post (Boolean_EXPRESSION);
+         --  pragma Post_Class (Boolean_EXPRESSION);
+
+         when Pragma_Post | Pragma_Post_Class => Post : declare
+            PC_Pragma : Node_Id;
+
+         begin
+            GNAT_Pragma;
+            Check_At_Least_N_Arguments (1);
+            Check_At_Most_N_Arguments (1);
+            Check_No_Identifiers;
+            Check_Pre_Post;
+
+            Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
+            PC_Pragma := New_Copy (N);
+            Set_Pragma_Identifier
+              (PC_Pragma, Make_Identifier (Loc, Name_Postcondition));
+            Rewrite (N, PC_Pragma);
+            Set_Analyzed (N, False);
+            Analyze (N);
+         end Post;
+
          -------------------
          -- Postcondition --
          -------------------
@@ -15090,6 +15204,32 @@ package body Sem_Prag is
             end if;
          end Postcondition;
 
+         -----------------
+         -- Pre[_Class] --
+         -----------------
+
+         --  pragma Pre (Boolean_EXPRESSION);
+         --  pragma Pre_Class (Boolean_EXPRESSION);
+
+         when Pragma_Pre | Pragma_Pre_Class => Pre : declare
+            PC_Pragma : Node_Id;
+
+         begin
+            GNAT_Pragma;
+            Check_At_Least_N_Arguments (1);
+            Check_At_Most_N_Arguments (1);
+            Check_No_Identifiers;
+            Check_Pre_Post;
+
+            Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
+            PC_Pragma := New_Copy (N);
+            Set_Pragma_Identifier
+              (PC_Pragma, Make_Identifier (Loc, Name_Precondition));
+            Rewrite (N, PC_Pragma);
+            Set_Analyzed (N, False);
+            Analyze (N);
+         end Pre;
+
          ------------------
          -- Precondition --
          ------------------
@@ -18405,6 +18545,7 @@ package body Sem_Prag is
       Subp_Id : Entity_Id)
    is
       Arg1 : constant Node_Id := First (Pragma_Argument_Associations (Prag));
+      Nam  : constant Name_Id := Original_Aspect_Name (Prag);
       Expr : Node_Id;
 
       Restore_Scope : Boolean := False;
@@ -18540,14 +18681,37 @@ package body Sem_Prag is
 
          begin
             if not Present (T) then
-               Error_Msg_Name_1 :=
-                 Chars (Identifier (Corresponding_Aspect (Prag)));
 
-               Error_Msg_Name_2 := Name_Class;
+               --  Pre'Class/Post'Class aspect cases
 
-               Error_Msg_N
-                 ("aspect `%''%` can only be specified for a primitive "
-                  & "operation of a tagged type", Corresponding_Aspect (Prag));
+               if From_Aspect_Specification (Prag) then
+                  if Nam = Name_uPre then
+                     Error_Msg_Name_1 := Name_Pre;
+                  else
+                     Error_Msg_Name_1 := Name_Post;
+                  end if;
+
+                  Error_Msg_Name_2 := Name_Class;
+
+                  Error_Msg_N
+                    ("aspect `%''%` can only be specified for a primitive "
+                     & "operation of a tagged type",
+                     Corresponding_Aspect (Prag));
+
+               --  Pre_Class, Post_Class pragma cases
+
+               else
+                  if Nam = Name_uPre then
+                     Error_Msg_Name_1 := Name_Pre_Class;
+                  else
+                     Error_Msg_Name_1 := Name_Post_Class;
+                  end if;
+
+                  Error_Msg_N
+                    ("pragma% can only be specified for a primitive "
+                     & "operation of a tagged type",
+                     Corresponding_Aspect (Prag));
+               end if;
             end if;
 
             Replace_Type (Get_Pragma_Arg (Arg1));
@@ -20073,7 +20237,7 @@ package body Sem_Prag is
       PP     : Node_Id;
       Policy : Name_Id;
 
-      Ename : constant Name_Id := Original_Name (N);
+      Ename : constant Name_Id := Original_Aspect_Name (N);
 
    begin
       --  No effect if not valid assertion kind name
@@ -20686,12 +20850,16 @@ package body Sem_Prag is
       Pragma_Passive                        => -1,
       Pragma_Persistent_BSS                 =>  0,
       Pragma_Polling                        => -1,
+      Pragma_Post                           => -1,
       Pragma_Postcondition                  => -1,
+      Pragma_Post_Class                     => -1,
+      Pragma_Pre                            => -1,
       Pragma_Precondition                   => -1,
       Pragma_Predicate                      => -1,
       Pragma_Preelaborable_Initialization   => -1,
       Pragma_Preelaborate                   => -1,
       Pragma_Preelaborate_05                => -1,
+      Pragma_Pre_Class                      => -1,
       Pragma_Priority                       => -1,
       Pragma_Priority_Specific_Dispatching  => -1,
       Pragma_Profile                        =>  0,
@@ -21023,66 +21191,6 @@ package body Sem_Prag is
       end if;
    end Make_Aspect_For_PPC_In_Gen_Sub_Decl;
 
-   -------------------
-   -- Original_Name --
-   -------------------
-
-   function Original_Name (N : Node_Id) return Name_Id is
-      Pras : Node_Id;
-      Name : Name_Id;
-
-   begin
-      pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma));
-      Pras := N;
-
-      if Is_Rewrite_Substitution (Pras)
-        and then Nkind (Original_Node (Pras)) = N_Pragma
-      then
-         Pras := Original_Node (Pras);
-      end if;
-
-      --  Case where we came from aspect specication
-
-      if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then
-         Pras := Corresponding_Aspect (Pras);
-      end if;
-
-      --  Get name from aspect or pragma
-
-      if Nkind (Pras) = N_Pragma then
-         Name := Pragma_Name (Pras);
-      else
-         Name := Chars (Identifier (Pras));
-      end if;
-
-      --  Deal with 'Class
-
-      if Class_Present (Pras) then
-         case Name is
-
-         --  Names that need converting to special _xxx form
-
-            when Name_Pre             => Name := Name_uPre;
-            when Name_Post            => Name := Name_uPost;
-            when Name_Invariant       => Name := Name_uInvariant;
-            when Name_Type_Invariant  => Name := Name_uType_Invariant;
-
-               --  Names already in special _xxx form (leave them alone)
-
-            when Name_uPre            => null;
-            when Name_uPost           => null;
-            when Name_uInvariant      => null;
-            when Name_uType_Invariant => null;
-
-               --  Anything else is impossible with Class_Present set True
-
-            when others               => raise Program_Error;
-         end case;
-      end if;
-
-      return Name;
-   end Original_Name;
-
    -------------------------
    -- Preanalyze_CTC_Args --
    -------------------------
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 7a0341bf67c..80ba002a711 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -215,6 +215,7 @@ package body Sem_Util is
    procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id) is
       Items : constant Node_Id := Contract (Subp_Id);
       Nam   : Name_Id;
+      N     : Node_Id;
 
    begin
       --  The related subprogram [body] must have a contract and the item to be
@@ -223,7 +224,7 @@ package body Sem_Util is
       pragma Assert (Present (Items));
       pragma Assert (Nkind (Prag) = N_Pragma);
 
-      Nam := Pragma_Name (Prag);
+      Nam := Original_Aspect_Name (Prag);
 
       --  Contract items related to subprogram bodies
 
@@ -241,7 +242,41 @@ package body Sem_Util is
       --  Contract items related to subprogram declarations
 
       else
-         if Nam_In (Nam, Name_Precondition, Name_Postcondition) then
+         if Nam_In (Nam, Name_Precondition,
+                         Name_Postcondition,
+                         Name_Pre,
+                         Name_Post,
+                         Name_uPre,
+                         Name_uPost)
+         then
+            --  Before we add a precondition or postcondition to the list,
+            --  make sure we do not have a disallowed duplicate, which can
+            --  happen if we use a pragma for Pre{_Class] or Post[_Class]
+            --  instead of the corresponding aspect.
+
+            if not From_Aspect_Specification (Prag)
+              and then Nam_In (Nam, Name_Pre_Class,
+                                    Name_Pre,
+                                    Name_uPre,
+                                    Name_Post_Class,
+                                    Name_Post,
+                                    Name_uPost)
+            then
+               N := Pre_Post_Conditions (Items);
+               while Present (N) loop
+                  if not Split_PPC (N)
+                    and then Original_Aspect_Name (N) = Nam
+                  then
+                     Error_Msg_Sloc := Sloc (N);
+                     Error_Msg_NE
+                       ("duplication of aspect for & given#", Prag, Subp_Id);
+                     return;
+                  else
+                     N := Next_Pragma (N);
+                  end if;
+               end loop;
+            end if;
+
             Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
             Set_Pre_Post_Conditions (Items, Prag);
 
@@ -4411,7 +4446,6 @@ package body Sem_Util is
 
    procedure Ensure_Freeze_Node (E : Entity_Id) is
       FN : Node_Id;
-
    begin
       if No (Freeze_Node (E)) then
          FN := Make_Freeze_Entity (Sloc (E));
@@ -4704,9 +4738,14 @@ package body Sem_Util is
       --  Inherited discriminants and components in derived record types are
       --  immediately visible. Itypes are not.
 
+      --  Unless the Itype is for a record type with a corresponding remote
+      --  type (what is that about, it was not commented ???)
+
       if Ekind_In (Def_Id, E_Discriminant, E_Component)
-        or else (No (Corresponding_Remote_Type (Def_Id))
-                 and then not Is_Itype (Def_Id))
+        or else
+          ((not Is_Record_Type (Def_Id)
+             or else No (Corresponding_Remote_Type (Def_Id)))
+            and then not Is_Itype (Def_Id))
       then
          Set_Is_Immediately_Visible (Def_Id);
          Set_Current_Entity         (Def_Id);
@@ -12833,6 +12872,71 @@ package body Sem_Util is
       end if;
    end Object_Access_Level;
 
+   --------------------------
+   -- Original_Aspect_Name --
+   --------------------------
+
+   function Original_Aspect_Name (N : Node_Id) return Name_Id is
+      Pras : Node_Id;
+      Name : Name_Id;
+
+   begin
+      pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma));
+      Pras := N;
+
+      if Is_Rewrite_Substitution (Pras)
+        and then Nkind (Original_Node (Pras)) = N_Pragma
+      then
+         Pras := Original_Node (Pras);
+      end if;
+
+      --  Case where we came from aspect specication
+
+      if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then
+         Pras := Corresponding_Aspect (Pras);
+      end if;
+
+      --  Get name from aspect or pragma
+
+      if Nkind (Pras) = N_Pragma then
+         Name := Pragma_Name (Pras);
+      else
+         Name := Chars (Identifier (Pras));
+      end if;
+
+      --  Deal with 'Class
+
+      if Class_Present (Pras) then
+         case Name is
+
+         --  Names that need converting to special _xxx form
+
+            when Name_Pre                  |
+                 Name_Pre_Class            =>
+               Name := Name_uPre;
+
+            when Name_Post                 |
+                 Name_Post_Class           =>
+               Name := Name_uPost;
+
+            when Name_Invariant            =>
+               Name := Name_uInvariant;
+
+            when Name_Type_Invariant       |
+                 Name_Type_Invariant_Class =>
+               Name := Name_uType_Invariant;
+
+            --  Nothing to do for other cases (e.g. a Check that derived
+            --  from Pre_Class and has the flag set). Also we do nothing
+            --  if the name is already in special _xxx form.
+
+            when others                    =>
+               null;
+         end case;
+      end if;
+
+      return Name;
+   end Original_Aspect_Name;
    --------------------------------------
    -- Original_Corresponding_Operation --
    --------------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 621cb01d2d9..13ee3b3dbe3 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1365,6 +1365,16 @@ package Sem_Util is
    --  convenience, qualified expressions applied to object names are also
    --  allowed as actuals for this function.
 
+   function Original_Aspect_Name (N : Node_Id) return Name_Id;
+   --  N is a pragma node or aspect specification node. This function returns
+   --  the name of the pragma or aspect in original source form, taking into
+   --  account possible rewrites, and also cases where a pragma comes from an
+   --  aspect (in such cases, the name can be different from the pragma name,
+   --  e.g. a Pre aspect generates a Precondition pragma). This also deals with
+   --  the presence of 'Class, which results in one of the special names
+   --  Name_uPre, Name_uPost, Name_uInvariant, or Name_uType_Invariant being
+   --  returned to represent the corresponding aspects with x'Class names.
+
    function Primitive_Names_Match (E1, E2 : Entity_Id) return Boolean;
    --  Returns True if the names of both entities correspond with matching
    --  primitives. This routine includes support for the case in which one
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index ceb50f848cd..aacaf8a505f 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -142,11 +142,10 @@ package Snames is
    Name_Dimension                      : constant Name_Id := N + $;
    Name_Dimension_System               : constant Name_Id := N + $;
    Name_Dynamic_Predicate              : constant Name_Id := N + $;
-   Name_Post                           : constant Name_Id := N + $;
-   Name_Pre                            : constant Name_Id := N + $;
    Name_Static_Predicate               : constant Name_Id := N + $;
    Name_Synchronization                : constant Name_Id := N + $;
    Name_Type_Invariant                 : constant Name_Id := N + $;
+   Name_Type_Invariant_Class           : constant Name_Id := N + $;
 
    --  Some special names used by the expander. Note that the lower case u's
    --  at the start of these names get translated to extra underscores. These
@@ -562,12 +561,16 @@ package Snames is
    Name_Pack                           : constant Name_Id := N + $;
    Name_Page                           : constant Name_Id := N + $;
    Name_Passive                        : constant Name_Id := N + $; -- GNAT
+   Name_Post                           : constant Name_Id := N + $; -- GNAT
    Name_Postcondition                  : constant Name_Id := N + $; -- GNAT
+   Name_Post_Class                     : constant Name_Id := N + $; -- GNAT
+   Name_Pre                            : constant Name_Id := N + $; -- GNAT
    Name_Precondition                   : constant Name_Id := N + $; -- GNAT
    Name_Predicate                      : constant Name_Id := N + $; -- GNAT
    Name_Preelaborable_Initialization   : constant Name_Id := N + $; -- Ada 05
    Name_Preelaborate                   : constant Name_Id := N + $;
    Name_Preelaborate_05                : constant Name_Id := N + $; -- GNAT
+   Name_Pre_Class                      : constant Name_Id := N + $; -- GNAT
 
    --  Note: Priority is not in this list because its name matches the name of
    --  the corresponding attribute. However, it is included in the definition
@@ -1860,12 +1863,16 @@ package Snames is
       Pragma_Pack,
       Pragma_Page,
       Pragma_Passive,
+      Pragma_Post,
       Pragma_Postcondition,
+      Pragma_Post_Class,
+      Pragma_Pre,
       Pragma_Precondition,
       Pragma_Predicate,
       Pragma_Preelaborable_Initialization,
       Pragma_Preelaborate,
       Pragma_Preelaborate_05,
+      Pragma_Pre_Class,
       Pragma_Psect_Object,
       Pragma_Pure,
       Pragma_Pure_05,