Index: exp_prag.adb
===================================================================
--- exp_prag.adb	(revision 165316)
+++ exp_prag.adb	(working copy)
@@ -310,6 +310,9 @@ package body Exp_Prag is
       --  be able to handle the assert error (which would not be the case if a
       --  call is made to the Raise_Assert_Failure procedure).
 
+      --  We also generate the direct raise if the Suppress_Exception_Locations
+      --  is active, since we don't want to generate messages in this case.
+
       --  Note that the reason we do not always generate a direct raise is that
       --  the form in which the procedure is called allows for more efficient
       --  breakpointing of assertion errors.
@@ -320,9 +323,10 @@ package body Exp_Prag is
 
       --  Case where we generate a direct raise
 
-      if (Debug_Flag_Dot_G
+      if ((Debug_Flag_Dot_G
            or else Restriction_Active (No_Exception_Propagation))
-        and then Present (Find_Local_Handler (RTE (RE_Assert_Failure), N))
+          and then Present (Find_Local_Handler (RTE (RE_Assert_Failure), N)))
+        or else (Opt.Exception_Locations_Suppressed and then No (Arg3 (N)))
       then
          Rewrite (N,
            Make_If_Statement (Loc,
@@ -337,29 +341,55 @@ package body Exp_Prag is
       --  Case where we call the procedure
 
       else
-         --  First, we need to prepare the string argument
-
          --  If we have a message given, use it
 
          if Present (Arg3 (N)) then
-            Msg := Arg3 (N);
+            Msg := Get_Pragma_Arg (Arg3 (N));
 
-         --  Otherwise string is "name failed at location" except in the case
-         --  of Assertion where "name failed at" is omitted.
+         --  Here we have no string, so prepare one
 
          else
-            if Nam = Name_Assertion then
-               Name_Len := 0;
-            else
-               Get_Name_String (Nam);
-               Set_Casing (Identifier_Casing (Current_Source_File));
-               Add_Str_To_Name_Buffer (" failed at ");
-            end if;
-
-            Build_Location_String (Loc);
-            Msg :=
-              Make_String_Literal (Loc,
-                Strval => String_From_Name_Buffer);
+            declare
+               Msg_Loc : constant String := Build_Location_String (Loc);
+
+            begin
+               --  For Assert, we just use the location
+
+               if Nam = Name_Assertion then
+                  Name_Len := 0;
+
+                  --  For any check except Precondition/Postcondition, the
+                  --  string is "xxx failed at yyy" where xxx is the name of
+                  --  the check with current source file casing.
+
+               elsif Nam /= Name_Precondition
+                       and then
+                     Nam /= Name_Postcondition
+               then
+                  Get_Name_String (Nam);
+                  Set_Casing (Identifier_Casing (Current_Source_File));
+                  Add_Str_To_Name_Buffer (" failed at ");
+
+               --  For special case of Precondition/Postcondition the string is
+               --  "failed xx from yy" where xx is precondition/postcondition
+               --  in all lower case. The reason for this different wording is
+               --  that the failure is not at the point of occurrence of the
+               --  pragma, unlike the other Check cases.
+
+               else
+                  Get_Name_String (Nam);
+                  Insert_Str_In_Name_Buffer ("failed ", 1);
+                  Add_Str_To_Name_Buffer (" from ");
+               end if;
+
+               --  In all cases, add location string
+
+               Add_Str_To_Name_Buffer (Msg_Loc);
+
+               --  Build the message
+
+               Msg := Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len));
+            end;
          end if;
 
          --  Now rewrite as an if statement
@@ -373,7 +403,7 @@ package body Exp_Prag is
                Make_Procedure_Call_Statement (Loc,
                  Name =>
                    New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc),
-                 Parameter_Associations => New_List (Msg)))));
+                 Parameter_Associations => New_List (Relocate_Node (Msg))))));
       end if;
 
       Analyze (N);
Index: sinfo.adb
===================================================================
--- sinfo.adb	(revision 165356)
+++ sinfo.adb	(working copy)
@@ -2745,6 +2745,15 @@ package body Sinfo is
       return Node1 (N);
    end Specification;
 
+   function Split_PPC
+      (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Aspect_Specification
+        or else NT (N).Nkind = N_Pragma);
+      return Flag17 (N);
+   end Split_PPC;
+
    function Statements
       (N : Node_Id) return List_Id is
    begin
@@ -5706,6 +5715,15 @@ package body Sinfo is
       Set_Node1_With_Parent (N, Val);
    end Set_Specification;
 
+   procedure Set_Split_PPC
+      (N : Node_Id; Val : Boolean) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Aspect_Specification
+        or else NT (N).Nkind = N_Pragma);
+      Set_Flag17 (N, Val);
+   end Set_Split_PPC;
+
    procedure Set_Statements
       (N : Node_Id; Val : List_Id) is
    begin
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 165356)
+++ sinfo.ads	(working copy)
@@ -1689,6 +1689,14 @@ package Sinfo is
    --    source type entity for the unchecked conversion instantiation
    --    which gigi must do size validation for.
 
+   --  Split_PPC (Flag17)
+   --     When a Pre or Postaspect specification is processed, it is broken
+   --     into AND THEN sections. The left most section has Split_PPC set to
+   --     False, indicating that it is the original specification (e.g. for
+   --     posting errors). For other sections, Split_PPC is set to True.
+   --     This flag is set in both the N_Aspect_Specification node itself,
+   --     and in the pragma which is generated from this node.
+
    --  Static_Processing_OK (Flag4-Sem)
    --    Present in N_Aggregate nodes. When the Compile_Time_Known_Aggregate
    --    flag is set, the full value of the aggregate can be determined at
@@ -2037,7 +2045,8 @@ package Sinfo is
       --  Is_Delayed_Aspect (Flag14-Sem)
       --  Import_Interface_Present (Flag16-Sem)
       --  Aspect_Cancel (Flag11-Sem)
-      --  Class_Present (Flag6) (set False if not from Aspect with 'Class)
+      --  Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
+      --  Class_Present (Flag6) set if from Aspect with 'Class
 
       --  Note: we should have a section on what pragmas are passed on to
       --  the back end to be processed. This section should note that pragma
@@ -6442,9 +6451,15 @@ package Sinfo is
       --  Entity (Node4-Sem) entity to which the aspect applies
       --  Class_Present (Flag6) Set if 'Class present
       --  Next_Rep_Item (Node5-Sem)
+      --  Split_PPC (Flag17) Set if split pre/post attribute
 
       --  Note: Aspect_Specification is an Ada 2012 feature
 
+      --  Note: When a Pre or Post aspect specification is processed, it is
+      --  broken into AND THEN sections. The left most section has Split_PPC
+      --  set to False, indicating that it is the original specification (e.g.
+      --  for posting errors). For the other sections, Split_PPC is set True.
+
       ---------------------------------------------
       -- 13.4  Enumeration representation clause --
       ---------------------------------------------
@@ -8709,6 +8724,9 @@ package Sinfo is
    function Specification
      (N : Node_Id) return Node_Id;    -- Node1
 
+   function Split_PPC
+     (N : Node_Id) return Boolean;    -- Flag17
+
    function Statements
      (N : Node_Id) return List_Id;    -- List3
 
@@ -9654,6 +9672,9 @@ package Sinfo is
    procedure Set_Specification
      (N : Node_Id; Val : Node_Id);            -- Node1
 
+   procedure Set_Split_PPC
+     (N : Node_Id; Val : Boolean);            -- Flag17
+
    procedure Set_Statements
      (N : Node_Id; Val : List_Id);            -- List3
 
@@ -11744,6 +11765,7 @@ package Sinfo is
    pragma Inline (Shift_Count_OK);
    pragma Inline (Source_Type);
    pragma Inline (Specification);
+   pragma Inline (Split_PPC);
    pragma Inline (Statements);
    pragma Inline (Static_Processing_OK);
    pragma Inline (Storage_Pool);
@@ -12055,6 +12077,7 @@ package Sinfo is
    pragma Inline (Set_Shift_Count_OK);
    pragma Inline (Set_Source_Type);
    pragma Inline (Set_Specification);
+   pragma Inline (Set_Split_PPC);
    pragma Inline (Set_Statements);
    pragma Inline (Set_Static_Processing_OK);
    pragma Inline (Set_Storage_Pool);
Index: usage.adb
===================================================================
--- usage.adb	(revision 165353)
+++ usage.adb	(working copy)
@@ -438,6 +438,10 @@ begin
                                                   "elaboration pragma");
    Write_Line ("        L*   turn off warnings for missing " &
                                                   "elaboration pragma");
+   Write_Line ("        .l*  turn on info messages for inherited pre/" &
+                                                  "postconditions");
+   Write_Line ("        .L   turn off info messages for inherited pre/" &
+                                                  "postconditions");
    Write_Line ("        m+   turn on warnings for variable assigned " &
                                                   "but not read");
    Write_Line ("        M*   turn off warnings for variable assigned " &
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 165359)
+++ sem_prag.adb	(working copy)
@@ -58,6 +58,7 @@ with Sem_Ch6;  use Sem_Ch6;
 with Sem_Ch8;  use Sem_Ch8;
 with Sem_Ch12; use Sem_Ch12;
 with Sem_Ch13; use Sem_Ch13;
+with Sem_Disp; use Sem_Disp;
 with Sem_Dist; use Sem_Dist;
 with Sem_Elim; use Sem_Elim;
 with Sem_Eval; use Sem_Eval;
@@ -90,10 +91,9 @@ package body Sem_Prag is
    -- Common Handling of Import-Export Pragmas --
    ----------------------------------------------
 
-   --  In the following section, a number of Import_xxx and Export_xxx
-   --  pragmas are defined by GNAT. These are compatible with the DEC
-   --  pragmas of the same name, and all have the following common
-   --  form and processing:
+   --  In the following section, a number of Import_xxx and Export_xxx pragmas
+   --  are defined by GNAT. These are compatible with the DEC pragmas of the
+   --  same name, and all have the following common form and processing:
 
    --  pragma Export_xxx
    --        [Internal                 =>] LOCAL_NAME
@@ -1247,7 +1247,7 @@ package body Sem_Prag is
             if Nkind (P) = N_Aspect_Specification
               or else From_Aspect_Specification (P)
             then
-               Error_Msg_NE ("aspect% for & previously specified#", N, E);
+               Error_Msg_NE ("aspect% for & previously given#", N, E);
             else
                Error_Msg_NE ("pragma% for & duplicates pragma#", N, E);
             end if;
@@ -1529,33 +1529,58 @@ package body Sem_Prag is
 
             S := Defining_Unit_Name (Specification (PO));
 
-            --  Make sure we do not have the case of a pre/postcondition
-            --  pragma when the corresponding aspect is present. This is
-            --  never allowed. We allow either pragmas or aspects, not both.
+            --  Make sure we do not have the case of a precondition pragma when
+            --  the Pre'Class aspect is present.
 
             --  We do this by looking at pragmas already chained to the entity
             --  since the aspect derived pragma will be put on this list first.
 
-            if not From_Aspect_Specification (N) then
-               P := Spec_PPC_List (S);
-               while Present (P) loop
-                  if Pragma_Name (P) = Pragma_Name (N)
-                    and then From_Aspect_Specification (P)
-                  then
-                     Error_Msg_Sloc := Sloc (P);
-
-                     if Prag_Id = Pragma_Precondition then
-                        Error_Msg_Name_2 := Name_Pre;
-                     else
-                        Error_Msg_Name_2 := Name_Post;
+            if Pragma_Name (N) = Name_Precondition then
+               if not From_Aspect_Specification (N) then
+                  P := Spec_PPC_List (S);
+                  while Present (P) loop
+                     if Pragma_Name (P) = Name_Precondition
+                       and then From_Aspect_Specification (P)
+                       and then Class_Present (P)
+                     then
+                        Error_Msg_Sloc := Sloc (P);
+                        Error_Pragma
+                          ("pragma% not allowed, `Pre''Class` aspect given#");
                      end if;
 
-                     Error_Pragma
-                       ("pragma% not allowed, % aspect given#");
-                  end if;
+                     P := Next_Pragma (P);
+                  end loop;
+               end if;
+            end if;
 
-                  P := Next_Pragma (P);
-               end loop;
+            --  Similarly check for Pre with inherited Pre'Class. Note that
+            --  we cover the aspect case as well here.
+
+            if Pragma_Name (N) = Name_Precondition
+              and then not Class_Present (N)
+            then
+               declare
+                  Inherited : constant Subprogram_List :=
+                                Inherited_Subprograms (S);
+                  P         : Node_Id;
+
+               begin
+                  for J in Inherited'Range loop
+                     P := Spec_PPC_List (Inherited (J));
+                     while Present (P) loop
+                        if Pragma_Name (P) = Name_Precondition
+                          and then Class_Present (P)
+                        then
+                           Error_Msg_Sloc := Sloc (P);
+                           Error_Pragma
+                             ("pragma% not allowed, `Pre''Class` "
+                              & "aspect inherited from#");
+                        end if;
+
+                        P := Next_Pragma (P);
+                     end loop;
+                  end loop;
+               end;
             end if;
 
             --  Analyze the pragma unless it appears within a package spec,
@@ -1645,9 +1670,7 @@ package body Sem_Prag is
             if Operating_Mode /= Generate_Code
               or else Inside_A_Generic
             then
-
-               --  Analyze expression in pragma, for correctness
-               --  and for ASIS use.
+               --  Analyze pragma expression for correctness and for ASIS use
 
                Preanalyze_Spec_Expression
                  (Get_Pragma_Arg (Arg1), Standard_Boolean);
@@ -3639,7 +3662,7 @@ package body Sem_Prag is
                               Set_Mechanism_Value
                                 (Formal, Expression (Massoc));
 
-                              --  Set entity on identifier for ASIS
+                              --  Set entity on identifier (needed by ASIS)
 
                               Set_Entity (Choice, Formal);
 
@@ -3814,15 +3837,15 @@ package body Sem_Prag is
          elsif Is_Subprogram (Def_Id)
            or else Is_Generic_Subprogram (Def_Id)
          then
-            --  If the name is overloaded, pragma applies to all of the
-            --  denoted entities in the same declarative part.
+            --  If the name is overloaded, pragma applies to all of the denoted
+            --  entities in the same declarative part.
 
             Hom_Id := Def_Id;
             while Present (Hom_Id) loop
                Def_Id := Get_Base_Subprogram (Hom_Id);
 
-               --  Ignore inherited subprograms because the pragma will
-               --  apply to the parent operation, which is the one called.
+               --  Ignore inherited subprograms because the pragma will apply
+               --  to the parent operation, which is the one called.
 
                if Is_Overloadable (Def_Id)
                  and then Present (Alias (Def_Id))
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb	(revision 165357)
+++ sem_ch12.adb	(working copy)
@@ -2877,6 +2877,8 @@ package body Sem_Ch12 is
       End_Scope;
       Exit_Generic_Scope (Id);
       Generate_Reference_To_Formals (Id);
+
+      List_Inherited_Pre_Post_Aspects (Id);
       Analyze_Aspect_Specifications (N, Id, Aspect_Specifications (N));
    end Analyze_Generic_Subprogram_Declaration;
 
Index: sinput.adb
===================================================================
--- sinput.adb	(revision 165356)
+++ sinput.adb	(working copy)
@@ -238,6 +238,13 @@ package body Sinput is
       return;
    end Build_Location_String;
 
+   function Build_Location_String (Loc : Source_Ptr) return String is
+   begin
+      Name_Len := 0;
+      Build_Location_String (Loc);
+      return Name_Buffer (1 .. Name_Len);
+   end Build_Location_String;
+
    -----------------------
    -- Get_Column_Number --
    -----------------------
Index: errout.ads
===================================================================
--- errout.ads	(revision 165316)
+++ errout.ads	(working copy)
@@ -207,6 +207,10 @@ package Errout is
    --      The idea is that for any use of -gnatj, it will still be the case
    --      that a location reference appears only at the end of a line.
 
+   --      Note: the output of the string "at " is suppressed if the string
+   --      " from" or " from " immediately precedes the insertion character #.
+   --      Certain messages read better with from than at.
+
    --    Insertion character } (Right brace: insert type reference)
    --      The character } is replaced by a string describing the type
    --      referenced by the entity whose Id is stored in Error_Msg_Node_1.
Index: sinput.ads
===================================================================
--- sinput.ads	(revision 165356)
+++ sinput.ads	(working copy)
@@ -471,6 +471,10 @@ package Sinput is
    --  ASCII.NUL, with Name_Length indicating the length not including the
    --  terminating Nul.
 
+   function Build_Location_String (Loc : Source_Ptr) return String;
+   --  Functional form returning a string, which does not include a terminating
+   --  null character. The contents of Name_Buffer is destroyed.
+
    function Get_Column_Number (P : Source_Ptr) return Column_Number;
    --  The ones-origin column number of the specified Source_Ptr value is
    --  determined and returned. Tab characters if present are assumed to
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 165358)
+++ sem_ch6.adb	(working copy)
@@ -2766,7 +2766,7 @@ package body Sem_Ch6 is
          end if;
       end if;
 
-      Designator :=  Analyze_Subprogram_Specification (Specification (N));
+      Designator := Analyze_Subprogram_Specification (Specification (N));
       Generate_Definition (Designator);
 
       if Debug_Flag_C then
@@ -2916,6 +2916,7 @@ package body Sem_Ch6 is
          Write_Eol;
       end if;
 
+      List_Inherited_Pre_Post_Aspects (Designator);
       Analyze_Aspect_Specifications (N, Designator, Aspect_Specifications (N));
    end Analyze_Subprogram_Declaration;
 
@@ -6937,6 +6938,43 @@ package body Sem_Ch6 is
       end if;
    end Is_Non_Overriding_Operation;
 
+   -------------------------------------
+   -- List_Inherited_Pre_Post_Aspects --
+   -------------------------------------
+
+   procedure List_Inherited_Pre_Post_Aspects (E : Entity_Id) is
+   begin
+      if Opt.List_Inherited_Pre_Post
+        and then (Is_Subprogram (E) or else Is_Generic_Subprogram (E))
+      then
+         declare
+            Inherited : constant Subprogram_List :=
+                          Inherited_Subprograms (E);
+            P         : Node_Id;
+
+         begin
+            for J in Inherited'Range loop
+               P := Spec_PPC_List (Inherited (J));
+               while Present (P) loop
+                  Error_Msg_Sloc := Sloc (P);
+
+                  if Class_Present (P) and then not Split_PPC (P) then
+                     if Pragma_Name (P) = Name_Precondition then
+                        Error_Msg_N
+                          ("?info: & inherits `Pre''Class` aspect from #", E);
+                     else
+                        Error_Msg_N
+                          ("?info: & inherits `Post''Class` aspect from #", E);
+                     end if;
+                  end if;
+
+                  P := Next_Pragma (P);
+               end loop;
+            end loop;
+         end;
+      end if;
+   end List_Inherited_Pre_Post_Aspects;
+
    ------------------------------
    -- Make_Inequality_Operator --
    ------------------------------
@@ -8586,11 +8624,25 @@ package body Sem_Ch6 is
       Body_Id : Entity_Id)
    is
       Loc   : constant Source_Ptr := Sloc (N);
-      Plist : List_Id             := No_List;
       Prag  : Node_Id;
       Subp  : Entity_Id;
       Parms : List_Id;
 
+      Precond : Node_Id := Empty;
+      --  Set non-Empty if we prepend precondition to the declarations. This
+      --  is used to hook up inherited preconditions (adding the condition
+      --  expression with OR ELSE, and adding the message).
+
+      Inherited_Precond : Node_Id;
+      --  Precondition inherited from parent subprogram
+
+      Inherited : constant Subprogram_List :=
+                    Inherited_Subprograms (Spec_Id);
+      --  List of subprograms inherited by this subprogram, null if no Spec_Id
+
+      Plist : List_Id := No_List;
+      --  List of generated postconditions
+
       function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
       --  Prag contains an analyzed precondition or postcondition pragma. This
       --  function copies the pragma, changes it to the corresponding Check
@@ -8665,19 +8717,26 @@ package body Sem_Ch6 is
            Make_Identifier (Sloc (Prag),
              Chars => Name_Check));
 
-         --  If this is inherited case then the current message starts with
-         --  "failed p" and we change this to "failed inherited p".
+         --  If this is inherited case and the current message starts with
+         --  "failed p", we change it to "failed inherited p...".
 
          if Present (Pspec) then
-            String_To_Name_Buffer
-              (Strval (Expression (Last (Pragma_Argument_Associations (CP)))));
-            pragma Assert (Name_Buffer (1 .. 8) = "failed p");
-            Name_Len := Name_Len + 10;
-            Name_Buffer (17 .. Name_Len) := Name_Buffer (7 .. Name_Len - 10);
-            Name_Buffer (7 .. 16) := " inherited";
-            Set_Strval
-              (Expression (Last (Pragma_Argument_Associations (CP))),
-               String_From_Name_Buffer);
+            declare
+               Msg : constant Node_Id :=
+                       Last (Pragma_Argument_Associations (CP));
+
+            begin
+               if Chars (Msg) = Name_Message then
+                  String_To_Name_Buffer (Strval (Expression (Msg)));
+
+                  if Name_Buffer (1 .. 8) = "failed p" then
+                     Insert_Str_In_Name_Buffer ("inherited ", 8);
+                     Set_Strval
+                       (Expression (Last (Pragma_Argument_Associations (CP))),
+                        String_From_Name_Buffer);
+                  end if;
+               end if;
+            end;
          end if;
 
          --  Return the check pragma
@@ -8688,12 +8747,6 @@ package body Sem_Ch6 is
    --  Start of processing for Process_PPCs
 
    begin
-      --  Nothing to do if we are not generating code
-
-      if Operating_Mode /= Generate_Code then
-         return;
-      end if;
-
       --  Grab preconditions from spec
 
       if Present (Spec_Id) then
@@ -8707,16 +8760,115 @@ package body Sem_Ch6 is
             if Pragma_Name (Prag) = Name_Precondition
               and then Pragma_Enabled (Prag)
             then
-               --  Add pragma Check at the start of the declarations of N.
-               --  Note that this processing reverses the order of the list,
-               --  which is what we want since new entries were chained to
-               --  the head of the list.
-
-               Prepend (Grab_PPC, Declarations (N));
+               --  For Pre (or Precondition pragma), we simply prepend the
+               --  pragma to the list of declarations right away so that it
+               --  will be executed at the start of the procedure. Note that
+               --  this processing reverses the order of the list, which is
+               --  what we want since new entries were chained to the head of
+               --  the list. There can be more then one precondition when we
+               --  use pragma Precondition
+
+               if not Class_Present (Prag) then
+                  Prepend (Grab_PPC, Declarations (N));
+
+               --  For Pre'Class there can only be one pragma, and we save
+               --  it in Precond for now. We will add inherited Pre'Class
+               --  stuff before inserting this pragma in the declarations.
+               else
+                  Precond := Grab_PPC;
+               end if;
             end if;
 
             Prag := Next_Pragma (Prag);
          end loop;
+
+         --  Now deal with inherited preconditions
+
+         for J in Inherited'Range loop
+            Prag := Spec_PPC_List (Inherited (J));
+
+            while Present (Prag) loop
+               if Pragma_Name (Prag) = Name_Precondition
+                 and then Class_Present (Prag)
+               then
+                  Inherited_Precond := Grab_PPC;
+
+                  --  No precondition so far, so establish this as the first
+
+                  if No (Precond) then
+                     Precond := Inherited_Precond;
+
+                  --  Here we already have a precondition, add inherited one
+
+                  else
+                     --  Add new precondition to old one using OR ELSE
+
+                     declare
+                        New_Expr : constant Node_Id :=
+                                     Get_Pragma_Arg
+                                       (Next
+                                         (First
+                                           (Pragma_Argument_Associations
+                                             (Inherited_Precond))));
+                        Old_Expr : constant Node_Id :=
+                                     Get_Pragma_Arg
+                                       (Next
+                                         (First
+                                           (Pragma_Argument_Associations
+                                             (Precond))));
+
+                     begin
+                        if Paren_Count (Old_Expr) = 0 then
+                           Set_Paren_Count (Old_Expr, 1);
+                        end if;
+
+                        if Paren_Count (New_Expr) = 0 then
+                           Set_Paren_Count (New_Expr, 1);
+                        end if;
+
+                        Rewrite (Old_Expr,
+                          Make_Or_Else (Sloc (Old_Expr),
+                            Left_Opnd  => Relocate_Node (Old_Expr),
+                            Right_Opnd => New_Expr));
+                     end;
+
+                     --  Add new message in the form:
+
+                     --     failed precondition from bla
+                     --       also failed inherited precondition from bla
+                     --       ...
+
+                     declare
+                        New_Msg : constant Node_Id :=
+                                    Get_Pragma_Arg
+                                      (Last
+                                        (Pragma_Argument_Associations
+                                          (Inherited_Precond)));
+                        Old_Msg : constant Node_Id :=
+                                    Get_Pragma_Arg
+                                      (Last
+                                        (Pragma_Argument_Associations
+                                          (Precond)));
+                     begin
+                        Start_String (Strval (Old_Msg));
+                        Store_String_Chars (ASCII.LF & "  also ");
+                        Store_String_Chars (Strval (New_Msg));
+                        Set_Strval (Old_Msg, End_String);
+                     end;
+                  end if;
+               end if;
+
+               Prag := Next_Pragma (Prag);
+            end loop;
+         end loop;
+
+         --  If we have built a precondition for Pre'Class (including any
+         --  Pre'Class aspects inherited from parent subprograms), then we
+         --  insert this composite precondition at this stage.
+
+         if Present (Precond) then
+            Prepend (Precond, Declarations (N));
+         end if;
       end if;
 
       --  Build postconditions procedure if needed and prepend the following
@@ -8779,8 +8931,6 @@ package body Sem_Ch6 is
 
       if Present (Spec_Id) then
          declare
-            Parent_Op : Node_Id;
-
             procedure Process_Post_Conditions
               (Spec  : Node_Id;
                Class : Boolean);
@@ -8836,17 +8986,11 @@ package body Sem_Ch6 is
                Process_Post_Conditions (Spec_Id, Class => False);
             end if;
 
-            --  Process directly inherited specifications
+            --  Process inherited postconditions
 
-            Parent_Op := Spec_Id;
-            loop
-               Parent_Op := Overridden_Operation (Parent_Op);
-               exit when No (Parent_Op);
-
-               if Ekind (Parent_Op) /= E_Enumeration_Literal
-                 and then Present (Spec_PPC_List (Parent_Op))
-               then
-                  Process_Post_Conditions (Parent_Op, Class => True);
+            for J in Inherited'Range loop
+               if Present (Spec_PPC_List (Inherited (J))) then
+                  Process_Post_Conditions (Inherited (J), Class => True);
                end if;
             end loop;
          end;
Index: sem_ch6.ads
===================================================================
--- sem_ch6.ads	(revision 165316)
+++ sem_ch6.ads	(working copy)
@@ -190,6 +190,10 @@ package Sem_Ch6 is
    --  conformant, and Prim is defined in the scope of Tagged_Type. Special
    --  management is done for functions returning interfaces.
 
+   procedure List_Inherited_Pre_Post_Aspects (E : Entity_Id);
+   --  E is the entity for a subprogram or generic subprogram spec. This call
+   --  lists all inherited Pre/Post aspects if List_Inherited_Pre_Post is True.
+
    function Mode_Conformant (New_Id, Old_Id : Entity_Id) return Boolean;
    --  Determine whether two callable entities (subprograms, entries,
    --  literals) are mode conformant (RM 6.3.1(15))
Index: namet.adb
===================================================================
--- namet.adb	(revision 165316)
+++ namet.adb	(working copy)
@@ -867,6 +867,19 @@ package body Namet is
       null;
    end Initialize;
 
+   -------------------------------
+   -- Insert_Str_In_Name_Buffer --
+   -------------------------------
+
+   procedure Insert_Str_In_Name_Buffer (S : String; Index : Positive) is
+      SL : constant Natural := S'Length;
+   begin
+      Name_Buffer (Index + SL .. Name_Len + SL) :=
+        Name_Buffer (Index .. Name_Len);
+      Name_Buffer (Index .. Index + SL - 1) := S;
+      Name_Len := Name_Len + SL;
+   end Insert_Str_In_Name_Buffer;
+
    ----------------------
    -- Is_Internal_Name --
    ----------------------
Index: namet.ads
===================================================================
--- namet.ads	(revision 165316)
+++ namet.ads	(working copy)
@@ -350,6 +350,11 @@ package Namet is
    --  Add characters of string S to the end of the string currently stored
    --  in the Name_Buffer, incrementing Name_Len by the length of the string.
 
+   procedure Insert_Str_In_Name_Buffer (S : String; Index : Positive);
+   --  Inserts given string in name buffer, starting at Index. Any existing
+   --  characters at or past this location get moved beyond the inserted string
+   --  and Name_Len is incremented by the length of the string.
+
    procedure Set_Character_Literal_Name (C : Char_Code);
    --  This procedure sets the proper encoded name for the character literal
    --  for the given character code. On return Name_Buffer and Name_Len are
Index: sem_warn.adb
===================================================================
--- sem_warn.adb	(revision 165316)
+++ sem_warn.adb	(working copy)
@@ -3068,6 +3068,7 @@ package body Sem_Warn is
             Elab_Warnings                       := True;
             Implementation_Unit_Warnings        := True;
             Ineffective_Inline_Warnings         := True;
+            List_Inherited_Pre_Post             := True;
             Warn_On_Ada_2005_Compatibility      := True;
             Warn_On_Ada_2012_Compatibility      := True;
             Warn_On_All_Unread_Out_Parameters   := True;
@@ -3113,6 +3114,12 @@ package body Sem_Warn is
          when 'I' =>
             Warn_On_Overlap                     := False;
 
+         when 'l' =>
+            List_Inherited_Pre_Post             := True;
+
+         when 'L' =>
+            List_Inherited_Pre_Post             := False;
+
          when 'm' =>
             Warn_On_Suspicious_Modulus_Value    := True;
 
@@ -3189,6 +3196,7 @@ package body Sem_Warn is
       Elab_Warnings                       := False;
       Implementation_Unit_Warnings        := False;
       Ineffective_Inline_Warnings         := True;
+      List_Inherited_Pre_Post             := False;
       Warn_On_Ada_2005_Compatibility      := True;
       Warn_On_Ada_2012_Compatibility      := True;
       Warn_On_All_Unread_Out_Parameters   := False;
@@ -3231,6 +3239,7 @@ package body Sem_Warn is
             Constant_Condition_Warnings         := True;
             Implementation_Unit_Warnings        := True;
             Ineffective_Inline_Warnings         := True;
+            List_Inherited_Pre_Post             := True;
             Warn_On_Ada_2005_Compatibility      := True;
             Warn_On_Ada_2012_Compatibility      := True;
             Warn_On_Assertion_Failure           := True;
@@ -3261,6 +3270,7 @@ package body Sem_Warn is
             Elab_Warnings                       := False;
             Implementation_Unit_Warnings        := False;
             Ineffective_Inline_Warnings         := False;
+            List_Inherited_Pre_Post             := False;
             Warn_On_Ada_2005_Compatibility      := False;
             Warn_On_Ada_2012_Compatibility      := False;
             Warn_On_All_Unread_Out_Parameters   := False;
Index: opt.ads
===================================================================
--- opt.ads	(revision 165316)
+++ opt.ads	(working copy)
@@ -729,6 +729,11 @@ package Opt is
    --  Set to True to skip compile and bind steps (except when Bind_Only is
    --  set to True).
 
+   List_Inherited_Pre_Post : Boolean := True;
+   --  GNAT
+   --  List inherited preconditions and postconditions from Pre'Class and
+   --  Post'Class aspects for ancestor subprograms.
+
    List_Restrictions : Boolean := False;
    --  GNATBIND
    --  Set to True to list restrictions pragmas that could apply to partition
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 165356)
+++ sem_ch13.adb	(working copy)
@@ -667,12 +667,14 @@ package body Sem_Ch13 is
             Loc  : constant Source_Ptr := Sloc (Aspect);
             Id   : constant Node_Id    := Identifier (Aspect);
             Expr : constant Node_Id    := Expression (Aspect);
-            Eloc :          Source_Ptr := Sloc (Expr);
             Nam  : constant Name_Id    := Chars (Id);
             A_Id : constant Aspect_Id  := Get_Aspect_Id (Nam);
             Anod : Node_Id;
             T    : Entity_Id;
 
+            Eloc : Source_Ptr := Sloc (Expr);
+            --  Source location of expression, modified when we split PPC's
+
          begin
             Set_Entity (Aspect, E);
             Ent := New_Occurrence_Of (E, Sloc (Id));
@@ -688,8 +690,41 @@ package body Sem_Ch13 is
                then
                   Error_Msg_Name_1 := Nam;
                   Error_Msg_Sloc := Sloc (Anod);
-                  Error_Msg_NE
-                    ("aspect% for & ignored, already given at#", Id, E);
+
+                  --  Case of same aspect specified twice
+
+                  if Class_Present (Anod) = Class_Present (Aspect) then
+                     if not Class_Present (Anod) then
+                        Error_Msg_NE
+                          ("aspect% for & previously given#",
+                           Id, E);
+                     else
+                        Error_Msg_NE
+                          ("aspect `%''Class` for & previously given#",
+                           Id, E);
+                     end if;
+
+                  --  Case of Pre and Pre'Class both specified
+
+                  elsif Nam = Name_Pre then
+                     if Class_Present (Aspect) then
+                        Error_Msg_NE
+                          ("aspect `Pre''Class` for & is not allowed here",
+                           Id, E);
+                        Error_Msg_NE
+                          ("\since aspect `Pre` previously given#",
+                           Id, E);
+
+                     else
+                        Error_Msg_NE
+                          ("aspect `Pre` for & is not allowed here",
+                           Id, E);
+                        Error_Msg_NE
+                          ("\since aspect `Pre''Class` previously given#",
+                           Id, E);
+                     end if;
+                  end if;
+
                   goto Continue;
                end if;
 
@@ -872,7 +907,6 @@ package body Sem_Ch13 is
 
                when Aspect_Pre | Aspect_Post => declare
                   Pname : Name_Id;
-                  Msg   : Node_Id;
 
                begin
                   if A_Id = Aspect_Pre then
@@ -886,26 +920,25 @@ package body Sem_Ch13 is
                   --  clauses. Since we allow multiple pragmas, there is no
                   --  problem in allowing multiple Pre/Post aspects internally.
 
-                  while Nkind (Expr) = N_And_Then loop
-                     Insert_After (Aspect,
-                       Make_Aspect_Specification (Sloc (Right_Opnd (Expr)),
-                         Identifier    => Identifier (Aspect),
-                         Expression    => Relocate_Node (Right_Opnd (Expr)),
-                         Class_Present => Class_Present (Aspect)));
-                     Rewrite (Expr, Relocate_Node (Left_Opnd (Expr)));
-                     Eloc := Sloc (Expr);
-                  end loop;
-
-                  --  Proceed with handling what's left after this split up
+                  --  We do not do this for Pre'Class, since we have to put
+                  --  these conditions together in a complex OR expression
 
-                  Msg :=
-                    Make_String_Literal (Eloc,
-                      Strval => "failed "
-                                  & Get_Name_String (Pname)
-                                  & " from line "
-                                  & Get_Logical_Line_Number_Img (Eloc));
+                  if Pname = Name_Postcondition
+                       or else not Class_Present (Aspect)
+                  then
+                     while Nkind (Expr) = N_And_Then loop
+                        Insert_After (Aspect,
+                          Make_Aspect_Specification (Sloc (Right_Opnd (Expr)),
+                            Identifier    => Identifier (Aspect),
+                            Expression    => Relocate_Node (Right_Opnd (Expr)),
+                            Class_Present => Class_Present (Aspect),
+                            Split_PPC     => True));
+                        Rewrite (Expr, Relocate_Node (Left_Opnd (Expr)));
+                        Eloc := Sloc (Expr);
+                     end loop;
+                  end if;
 
-                  --  Construct the pragma
+                  --  Build the precondition/postcondition pragma
 
                   Aitem :=
                     Make_Pragma (Loc,
@@ -913,13 +946,25 @@ package body Sem_Ch13 is
                         Make_Identifier (Sloc (Id),
                           Chars => Pname),
                       Class_Present                => Class_Present (Aspect),
+                      Split_PPC                    => Split_PPC (Aspect),
                       Pragma_Argument_Associations => New_List (
                         Make_Pragma_Argument_Association (Eloc,
                           Chars      => Name_Check,
-                          Expression => Relocate_Node (Expr)),
-                        Make_Pragma_Argument_Association (Eloc,
-                          Chars      => Name_Message,
-                          Expression => Msg)));
+                          Expression => Relocate_Node (Expr))));
+
+                  --  Add message unless exception messages are suppressed
+
+                  if not Opt.Exception_Locations_Suppressed then
+                     Append_To (Pragma_Argument_Associations (Aitem),
+                       Make_Pragma_Argument_Association (Eloc,
+                         Chars     => Name_Message,
+                         Expression =>
+                           Make_String_Literal (Eloc,
+                             Strval => "failed "
+                                       & Get_Name_String (Pname)
+                                       & " from "
+                                       & Build_Location_String (Eloc))));
+                  end if;
 
                   Set_From_Aspect_Specification (Aitem, True);
 
@@ -1213,7 +1258,7 @@ package body Sem_Ch13 is
             if Entity (A) = U_Ent then
                Error_Msg_Name_1 := Chars (N);
                Error_Msg_Sloc := Sloc (A);
-               Error_Msg_NE ("aspect% for & previously specified#", N, U_Ent);
+               Error_Msg_NE ("aspect% for & previously given#", N, U_Ent);
                return True;
             end if;
          end if;
Index: erroutc.adb
===================================================================
--- erroutc.adb	(revision 165316)
+++ erroutc.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2009, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -717,11 +717,31 @@ package body Erroutc is
       Sindex_Loc  : Source_File_Index;
       Sindex_Flag : Source_File_Index;
 
+      procedure Set_At;
+      --  Outputs "at " unless last characters in buffer are " from ". Certain
+      --  messages read better with from than at.
+
+      ------------
+      -- Set_At --
+      ------------
+
+      procedure Set_At is
+      begin
+         if Msglen < 6
+           or else Msg_Buffer (Msglen - 5 .. Msglen) /= " from "
+         then
+            Set_Msg_Str ("at ");
+         end if;
+      end Set_At;
+
+   --  Start of processing for Set_Msg_Insertion_Line_Number
+
    begin
       Set_Msg_Blank;
 
       if Loc = No_Location then
-         Set_Msg_Str ("at unknown location");
+         Set_At;
+         Set_Msg_Str ("unknown location");
 
       elsif Loc = System_Location then
          Set_Msg_Str ("in package System");
@@ -743,7 +763,7 @@ package body Erroutc is
          Sindex_Flag := Get_Source_File_Index (Flag);
 
          if Full_File_Name (Sindex_Loc) /= Full_File_Name (Sindex_Flag) then
-            Set_Msg_Str ("at ");
+            Set_At;
             Get_Name_String
               (Reference_Name (Get_Source_File_Index (Loc)));
             Set_Msg_Name_Buffer;
@@ -752,7 +772,8 @@ package body Erroutc is
          --  If in current file, add text "at line "
 
          else
-            Set_Msg_Str ("at line ");
+            Set_At;
+            Set_Msg_Str ("line ");
          end if;
 
          --  Output line number for reference
Index: sem_disp.adb
===================================================================
--- sem_disp.adb	(revision 165316)
+++ sem_disp.adb	(working copy)
@@ -1727,6 +1727,47 @@ package body Sem_Disp is
    end Find_Primitive_Covering_Interface;
 
    ---------------------------
+   -- Inherited_Subprograms --
+   ---------------------------
+
+   function Inherited_Subprograms (S : Entity_Id) return Subprogram_List is
+      Result : Subprogram_List (1 .. 6000);
+      --  6000 here is intended to be infinity. We could use an expandable
+      --  table, but it would be awfully heavy, and there is no way that we
+      --  could reasonably exceed this value.
+
+      N : Int := 0;
+      --  Number of entries in Result
+
+      Parent_Op : Entity_Id;
+      --  Traverses the Overridden_Operation chain
+
+   begin
+      if Present (S) then
+
+         --  Deal with direct inheritance
+
+         Parent_Op := S;
+         loop
+            Parent_Op := Overridden_Operation (Parent_Op);
+            exit when No (Parent_Op);
+
+            if Is_Subprogram (Parent_Op)
+              or else Is_Generic_Subprogram (Parent_Op)
+            then
+               N := N + 1;
+               Result (N) := Parent_Op;
+            end if;
+         end loop;
+
+         --  For now don't bother with interfaces, TBD ???
+
+      end if;
+
+      return Result (1 .. N);
+   end Inherited_Subprograms;
+
+   ---------------------------
    -- Is_Dynamically_Tagged --
    ---------------------------
 
Index: sem_disp.ads
===================================================================
--- sem_disp.ads	(revision 165316)
+++ sem_disp.ads	(working copy)
@@ -93,6 +93,17 @@ package Sem_Disp is
    --  whose alias attribute references the interface primitive). If none of
    --  these entities is found then return Empty.
 
+   type Subprogram_List is array (Nat range <>) of Entity_Id;
+   --  Type returned by Inherited_Subprograms function
+
+   function Inherited_Subprograms (S : Entity_Id) return Subprogram_List;
+   --  Given the spec of a subprogram, this function gathers any inherited
+   --  subprograms from direct inheritance or via interfaces. The list is
+   --  a list of entity id's of the specs of inherited subprograms. Returns
+   --  a null array if passed an Empty spec id. Note that the returned array
+   --  only includes subprograms and generic subprograms (and excludes any
+   --  other inherited entities, in particular enumeration literals).
+
    function Is_Dynamically_Tagged (N : Node_Id) return Boolean;
    --  Used to determine whether a call is dispatching, i.e. if is an
    --  an expression of a class_Wide type, or a call to a function with
