Patchwork [Ada] Further work on pre/post aspects

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 12, 2010, 11:05 a.m.
Message ID <20101012110537.GA22298@adacore.com>
Download mbox | patch
Permalink /patch/67533/
State New
Headers show

Comments

Arnaud Charlet - Oct. 12, 2010, 11:05 a.m.
This patch implements a new warning switch -gnatw.l that causes
listing of inherited Pre/Post aspects, this is on by default.
It also does a general cleanup of error message handling for
Pre/Post attributes, and there is a complete implementation of
inherited Pre'Class attributes.

Still to be done in this AI:

Handle visibility right, the GNAT rules for pragmas do not
quite match the RM rules for Pre/Post aspects.

Deal with entries (not clear yet what is involved)

Fix error in handling inherited preconditions, these still
don't work, but it is helpful to checkin the current sources
to further investigate the problem.

Resolve the issue of 'Old restrictions

Tested on x86_64-pc-linux-gnu, committed on trunk

2010-10-12  Robert Dewar  <dewar@adacore.com>

	* errout.ads, erroutc.adb: The # insertion now handles from in place of
	at.
	* exp_prag.adb (Expand_Pragma_Check): Suppress generated default
	message if new switch Exception_Locations_Suppressed is set.
	(Expand_Pragma_Check): Revised wording for default message for case
	of precondition or postcondition.
	* namet.ads, namet.adb (Build_Location_String): New procedure.
	* opt.ads (List_Inherited_Pre_Post): New flag.
	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Add call to
	list inherited pre/post aspects.
	* sem_ch13.adb (Analyze_Aspect_Specification): Improve generation of
	messages for precondition/postcondition cases.
	* sem_ch6.adb (Process_PPCs): General cleanup, and list inherited PPC's
	if flag List_Inherited_Pre_Post is set True.
	(Process_PPCs): Add initial handling for inherited preconditions
	(List_Inherited_Pre_Post_Aspects): New procedure
	* sem_ch6.ads (List_Inherited_Pre_Post_Aspects): New procedure
	* sem_disp.adb (Inherited_Subprograms): New function
	* sem_disp.ads (Inherited_Subprograms): New function
	* sem_prag.adb (Check_Duplicate_Pragma): Clean up handling of
	pre/postcondition.
	(Check_Precondition_Postcondition): Check for inherited aspects
	* sem_warn.adb: Process -gnatw.l/w.L setting List_Inherited_Pre_Post
	* sinfo.ads, sinfo.adb (Split_PPC): New flag.
	* sinput.ads, sinput.adb (Build_Location_String): New function.
	* usage.adb: Add line for -gnatw.l/-gnatw.L

Patch

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