[Ada] Handle delay of Pre/Post and inherited Pre'Class

Submitted by Arnaud Charlet on Oct. 18, 2010, 9:42 a.m.

Details

Message ID 20101018094238.GA2819@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 18, 2010, 9:42 a.m. 
This patch completes two of the remaining issues in processing the
Pre/Post attributes. First inheritance of Pre'Class is properly
handled. Second, delay of visibility analysis of Pre/Post aspects
is done right for all declarative parts, not just packages.

The following test of Pre'Class inheritance is compiled with
-gnatld7 -gnatj60 -gnata12:

Compiling: test_prepost_ifaces.adb

     1. with Prepost_Ifaces.P123;
     2. use Prepost_Ifaces;
     3. use Prepost_Ifaces.P123;
     4. with Prepost_Ifaces.P1; use Prepost_Ifaces.P1;
     5. with Prepost_Ifaces.P2; use Prepost_Ifaces.P2;
     6. with Prepost_Ifaces.P3; use Prepost_Ifaces.P3;
     7. procedure Test_Prepost_Ifaces is
     8.    X123 : T123 := (null record);
     9.    X23 : T23 := (null record);
    10. begin
    11.    P1.Dispatch (X123);
    12.    P2.Dispatch (X123);
    13.    P3.Dispatch (X123);
    14.
    15.    P2.Dispatch (X23);
    16.    P3.Dispatch (X23);
    17. end Test_Prepost_Ifaces;

 17 lines: No errors

Compiling: prepost_ifaces.adb

     1. package body Prepost_Ifaces is
     2.
     3.    function Faux return Boolean is
     4.    begin
     5.       return False;
     6.    end Faux;
     7.
     8.    function Vrai return Boolean is
     9.    begin
    10.       return True;
    11.    end Vrai;
    12.
    13. end Prepost_Ifaces;

Compiling: prepost_ifaces.ads

     1. with Ada.Text_IO; use Ada.Text_IO;
     2. with Ada.Assertions; use Ada.Assertions;
     3. package Prepost_Ifaces is
     4.
     5.    function Faux return Boolean;
     6.    function Vrai return Boolean;
     7.
     8. end Prepost_Ifaces;

 13 lines: No errors

Compiling: prepost_ifaces-p1.adb

     1. with Ada.Exceptions; use Ada.Exceptions;
     2. package body Prepost_Ifaces.P1 is
     3.
     4.    procedure Dispatch (X : T1'Class) is
     5.    begin
     6.       OK_Pre (X);
     7.       OK_Post (X);
     8.
     9.       begin
    10.          Bad_Pre (X);
    11.          Put_Line ("P1: Bad_Pre: No exception");
    12.       exception
    13.          when E : Assertion_Error =>
    14.             Put_Line ("P1: Bad_Pre: Assertion_Error");
    15.             Put_Line ("  " & Exception_Message (E));
    16.       end;
    17.
    18.       begin
    19.          Bad_Post (X);
    20.          Put_Line
    21.            ("P1: Bad_Post: No exception");
    22.       exception
    23.          when E : Assertion_Error =>
    24.             Put_Line ("P1: Bad_Post: Assertion_Error");
    25.             Put_Line ("  " & Exception_Message (E));
    26.       end;
    27.    end Dispatch;
    28.
    29. end Prepost_Ifaces.P1;

Compiling: prepost_ifaces-p1.ads

     1. package Prepost_Ifaces.P1 is
     2.    type T1 is abstract tagged null record;
     3.    procedure OK_Pre (X : T1) is abstract with
     4.      Pre'Class => Faux;
     5.    procedure Bad_Pre (X : T1) is abstract with
     6.      Pre'Class => Faux;
     7.    procedure OK_Post (X : T1) is abstract with
     8.      Post'Class => Vrai;
     9.    procedure Bad_Post (X : T1) is abstract with
    10.      Post'Class => Vrai;
    11.
    12.    procedure Dispatch (X : T1'Class);
    13. end Prepost_Ifaces.P1;

 29 lines: No errors

Compiling: prepost_ifaces-p123.adb

     1. package body Prepost_Ifaces.P123 is
     2.
     3.    overriding procedure OK_Pre (X : T123) is
     4.    begin
     5.       null;
     6.    end OK_Pre;
     7.
     8.    overriding procedure Bad_Pre (X : T123) is
     9.    begin
    10.       null;
    11.    end Bad_Pre;
    12.
    13.    overriding procedure OK_Post (X : T123) is
    14.    begin
    15.       null;
    16.    end OK_Post;
    17.
    18.    overriding procedure Bad_Post (X : T123) is
    19.    begin
    20.       null;
    21.    end Bad_Post;
    22.
    23.    overriding procedure OK_Pre (X : T23) is
    24.    begin
    25.       null;
    26.    end OK_Pre;
    27.
    28.    overriding procedure Bad_Pre (X : T23) is
    29.    begin
    30.       null;
    31.    end Bad_Pre;
    32.
    33.    overriding procedure OK_Post (X : T23) is
    34.    begin
    35.       null;
    36.    end OK_Post;
    37.
    38.    overriding procedure Bad_Post (X : T23) is
    39.    begin
    40.       null;
    41.    end Bad_Post;
    42.
    43. end Prepost_Ifaces.P123;

Compiling: prepost_ifaces-p123.ads

     1. with Prepost_Ifaces.P1; use Prepost_Ifaces.P1;
     2. with Prepost_Ifaces.P2; use Prepost_Ifaces.P2;
     3. with Prepost_Ifaces.P3; use Prepost_Ifaces.P3;
     4. package Prepost_Ifaces.P123 is
     5.    type T123 is new T1 and T2 and T3
     6.      with null record;
     7.
     8.    overriding procedure OK_Pre (X : T123);
                                |
        >>> info: "OK_Pre" inherits "Pre'Class" aspect from
            prepost_ifaces-p1.ads:4

     9.    -- Inherits Pre => False or False or True
    10.
    11.    overriding procedure Bad_Pre (X : T123);
                                |
        >>> info: "Bad_Pre" inherits "Pre'Class" aspect
            from prepost_ifaces-p1.ads:6

    12.    -- Inherits Pre => False or False or False
    13.
    14.    overriding procedure OK_Post (X : T123);
                                |
        >>> info: "OK_Post" inherits "Post'Class" aspect
            from prepost_ifaces-p1.ads:8

    15.    -- Inherits Post => True and True and True
    16.
    17.    overriding procedure Bad_Post (X : T123);
                                |
        >>> info: "Bad_Post" inherits "Post'Class" aspect
            from prepost_ifaces-p1.ads:10

    18.    -- Inherits Post => True and True and False
    19.
    20.    type T23 is new T2 and T3 with null record;
    21.
    22.    overriding procedure OK_Pre (X : T23);
                                |
        >>> info: "OK_Pre" inherits "Pre'Class" aspect from
            prepost_ifaces-p2.ads:4

    23.    -- Inherits Pre => False or True
    24.
    25.    overriding procedure Bad_Pre (X : T23);
                                |
        >>> info: "Bad_Pre" inherits "Pre'Class" aspect
            from prepost_ifaces-p2.ads:6

    26.    -- Inherits Pre => False or False
    27.
    28.    overriding procedure OK_Post (X : T23);
                                |
        >>> info: "OK_Post" inherits "Post'Class" aspect
            from prepost_ifaces-p2.ads:8

    29.    -- Inherits Post => True and True
    30.
    31.    overriding procedure Bad_Post (X : T23);
                                |
        >>> info: "Bad_Post" inherits "Post'Class" aspect
            from prepost_ifaces-p2.ads:10

    32.    -- Inherits Post => True and False
    33.
    34. end Prepost_Ifaces.P123;


Compiling: prepost_ifaces-p2.adb

     1. with Ada.Exceptions; use Ada.Exceptions;
     2. package body Prepost_Ifaces.P2 is
     3.
     4.    procedure Dispatch (X : T2'Class) is
     5.    begin
     6.       OK_Pre (X);
     7.       OK_Post (X);
     8.
     9.       begin
    10.          Bad_Pre (X);
    11.          Put_Line ("P2: Bad_Pre: No exception");
    12.       exception
    13.          when E : Assertion_Error =>
    14.             Put_Line ("P2: Bad_Pre: Assertion_Error: ");
    15.             Put_Line ("  " & Exception_Message (E));
    16.       end;
    17.
    18.       begin
    19.          Bad_Post (X);
    20.          Put_Line ("P2: Bad_Post: No exception");
    21.       exception
    22.          when E : Assertion_Error =>
    23.             Put_Line ("P2: Bad_Post: Assertion_Error");
    24.             Put_Line ("  " & Exception_Message (E));
    25.       end;
    26.    end Dispatch;
    27.
    28. end Prepost_Ifaces.P2;

Compiling: prepost_ifaces-p2.ads

     1. package Prepost_Ifaces.P2 is
     2.    type T2 is interface;
     3.    procedure OK_Pre (X : T2) is abstract with
     4.      Pre'Class => Faux;
     5.    procedure Bad_Pre (X : T2) is abstract with
     6.      Pre'Class => Faux;
     7.    procedure OK_Post (X : T2) is abstract with
     8.      Post'Class => Vrai;
     9.    procedure Bad_Post (X : T2) is abstract with
    10.      Post'Class => Vrai;
    11.
    12.    procedure Dispatch (X : T2'Class);
    13. end Prepost_Ifaces.P2;

 28 lines: No errors

Compiling: prepost_ifaces-p3.adb

     1. with Ada.Exceptions; use Ada.Exceptions;
     2. package body Prepost_Ifaces.P3 is
     3.
     4.    procedure Dispatch (X : T3'Class) is
     5.    begin
     6.       OK_Pre (X);
     7.       OK_Post (X);
     8.
     9.       begin
    10.          Bad_Pre (X);
    11.          Put_Line
    12.            ("P3: Bad_Pre: No exception");
    13.       exception
    14.          when E : Assertion_Error =>
    15.             Put_Line ("P3: Bad_Pre: Assertion_Error");
    16.             Put_Line ("  " & Exception_Message (E));
    17.       end;
    18.
    19.       begin
    20.          Bad_Post (X);
    21.          Put_Line
    22.            ("P3: Bad_Post: No exception");
    23.       exception
    24.          when E : Assertion_Error =>
    25.             Put_Line ("P3: Bad_Post: Assertion_Error");
    26.             Put_Line ("  " & Exception_Message (E));
    27.       end;
    28.    end Dispatch;
    29.
    30. end Prepost_Ifaces.P3;

Compiling: prepost_ifaces-p3.ads

     1. package Prepost_Ifaces.P3 is
     2.    type T3 is interface;
     3.    procedure OK_Pre (X : T3) is null with
     4.      Pre'Class => Vrai;
     5.    procedure Bad_Pre (X : T3) is null with
     6.      Pre'Class => Faux;
     7.    procedure OK_Post (X : T3) is null with
     8.      Post'Class => Vrai;
     9.    procedure Bad_Post (X : T3) is null with
    10.      Post'Class => Faux;
    11.
    12.    procedure Dispatch (X : T3'Class);
    13. end Prepost_Ifaces.P3;

 30 lines: No errors

The output when this program is run is:

P1: Bad_Pre: Assertion_Error
  failed inherited precondition from prepost_ifaces-p1.ads:6
  also failed inherited precondition from prepost_ifaces-p2.ads:6
  also failed inherited precondition from prepost_ifaces-p3.ads:6
P1: Bad_Post: Assertion_Error
  failed inherited postcondition from prepost_ifaces-p3.ads:10
P2: Bad_Pre: Assertion_Error:
  failed inherited precondition from prepost_ifaces-p1.ads:6
  also failed inherited precondition from prepost_ifaces-p2.ads:6
  also failed inherited precondition from prepost_ifaces-p3.ads:6
P2: Bad_Post: Assertion_Error
  failed inherited postcondition from prepost_ifaces-p3.ads:10
P3: Bad_Pre: Assertion_Error
  failed inherited precondition from prepost_ifaces-p1.ads:6
  also failed inherited precondition from prepost_ifaces-p2.ads:6
  also failed inherited precondition from prepost_ifaces-p3.ads:6
P3: Bad_Post: Assertion_Error
  failed inherited postcondition from prepost_ifaces-p3.ads:10
P2: Bad_Pre: Assertion_Error:
  failed inherited precondition from prepost_ifaces-p2.ads:6
  also failed inherited precondition from prepost_ifaces-p3.ads:6
P2: Bad_Post: Assertion_Error
  failed inherited postcondition from prepost_ifaces-p3.ads:10
P3: Bad_Pre: Assertion_Error
  failed inherited precondition from prepost_ifaces-p2.ads:6
  also failed inherited precondition from prepost_ifaces-p3.ads:6
P3: Bad_Post: Assertion_Error
  failed inherited postcondition from prepost_ifaces-p3.ads:10

the following test shows proper delay of Pre/Post visibility in
a declarative part of a subprogram. Compiled with -gnata12 -gnatld7:

     1. with Text_IO; use Text_IO;
     2. with Ada.Exceptions;
     3. use Ada.Exceptions;
     4. procedure Prepostdelay is
     5.    procedure p1 (X : Integer) with
     6.      Pre => ident (X) = 13;
     7.
     8.    function ident (X : Integer) return Integer;
     9.
    10.    procedure p1 (X : Integer) is
    11.    begin null; end;
    12.
    13.    function ident (X : Integer) return Integer
    14.    is begin return X; end;
    15.
    16. begin
    17.    p1 (13);
    18.    Put_Line ("no exception for p1 (13)");
    19.    begin
    20.       p1 (12);
    21.    exception
    22.       when E : others =>
    23.          Put_Line ("exception for p1 (12)");
    24.          Put_Line ("  " & Exception_Message (E));
    25.    end;
    26. end Prepostdelay;

The output is:

no exception for p1 (13)
exception for p1 (12)
  failed precondition from prepostdelay.adb:6

The following test shows that the visibilty does not extend
into the private part, compiled again with -gnata12 -gnatld7

     1. package Prepostdelay2 is
     2.    procedure p1 (X : Integer) with
     3.      Pre => ident (X) = 13;
     4.
     5.    function ident (X : Integer) return Integer;
     6.
     7.    procedure p2 (X : Integer) with
     8.    Pre => ident2 (X);
                  |
        >>> "ident2" is undefined
        >>> possible misspelling of "ident"

     9.
    10. private
    11.    function ident2 (X : Integer) return Integer;
    12. end;

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

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

	* einfo.ads, einfo.adb (Spec_PPC_List): Is now present in Entries
	* sem_ch3.adb (Analyze_Declarations): Add processing for delaying
	visibility analysis of precondition and postcondition pragmas (and
	Pre/Post aspects).
	* sem_ch6.adb (Process_PPCs): Add handling of inherited Pre'Class
	aspects.
	* sem_ch7.adb (Analyze_Package_Specification): Remove special handling
	of pre/post conditions (no longer needed).
	* sem_disp.adb (Inherit_Subprograms): Deal with interface case.
	* sem_prag.adb (Analyze_PPC_In_Decl_Part): Remove analysis of message
	argument, since this is now done in the main processing for
	pre/postcondition pragmas when they are first seen.
	(Chain_PPC): Pre'Class and Post'Class now handled properly
	(Chain_PPC): Handle Pre/Post aspects for entries
	(Check_Precondition_Postcondition): Handle entry declaration case
	(Check_Precondition_Postcondition): Handle delay of visibility analysis
	(Check_Precondition_Postcondition): Preanalyze message argument if
	present.

Patch hide | download patch | download mbox 

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 165610)
+++ sem_ch3.adb	(working copy)
@@ -62,6 +62,7 @@  with Sem_Dist; use Sem_Dist;
 with Sem_Elim; use Sem_Elim;
 with Sem_Eval; use Sem_Eval;
 with Sem_Mech; use Sem_Mech;
+with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Smem; use Sem_Smem;
 with Sem_Type; use Sem_Type;
@@ -2069,6 +2070,35 @@  package body Sem_Ch3 is
 
          D := Next_Node;
       end loop;
+
+      --  One more thing to do, we need to scan the declarations to check
+      --  for any precondition/postcondition pragmas (Pre/Post aspects have
+      --  by this stage been converted into corresponding pragmas). It is
+      --  at this point that we analyze the expressions in such pragmas,
+      --  to implement the delayed visibility requirement.
+
+      declare
+         Decl : Node_Id;
+         Spec : Node_Id;
+         Sent : Entity_Id;
+         Prag : Node_Id;
+
+      begin
+         Decl := First (L);
+         while Present (Decl) loop
+            if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
+               Spec := Specification (Original_Node (Decl));
+               Sent := Defining_Unit_Name (Spec);
+               Prag := Spec_PPC_List (Sent);
+               while Present (Prag) loop
+                  Analyze_PPC_In_Decl_Part (Prag, Sent);
+                  Prag := Next_Pragma (Prag);
+               end loop;
+            end if;
+
+            Next (Decl);
+         end loop;
+      end;
    end Analyze_Declarations;
 
    -----------------------------------
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 165610)
+++ sem_ch7.adb	(working copy)
@@ -55,7 +55,6 @@  with Sem_Ch12; use Sem_Ch12;
 with Sem_Ch13; use Sem_Ch13;
 with Sem_Disp; use Sem_Disp;
 with Sem_Eval; use Sem_Eval;
-with Sem_Prag; use Sem_Prag;
 with Sem_Util; use Sem_Util;
 with Sem_Warn; use Sem_Warn;
 with Snames;   use Snames;
@@ -872,12 +871,6 @@  package body Sem_Ch7 is
       --  private_with_clauses, and remove them at the end of the nested
       --  package.
 
-      procedure Analyze_PPCs (Decls : List_Id);
-      --  Given a list of declarations, go through looking for subprogram
-      --  specs, and for each one found, analyze any pre/postconditions that
-      --  are chained to the spec. This is the implementation of the late
-      --  visibility analysis for preconditions and postconditions in specs.
-
       procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
       --  Clears constant indications (Never_Set_In_Source, Constant_Value, and
       --  Is_True_Constant) on all variables that are entities of Id, and on
@@ -906,33 +899,6 @@  package body Sem_Ch7 is
       --  private part rather than being done in Sem_Ch12.Install_Parent
       --  (which is where the parents' visible declarations are installed).
 
-      ------------------
-      -- Analyze_PPCs --
-      ------------------
-
-      procedure Analyze_PPCs (Decls : List_Id) is
-         Decl : Node_Id;
-         Spec : Node_Id;
-         Sent : Entity_Id;
-         Prag : Node_Id;
-
-      begin
-         Decl := First (Decls);
-         while Present (Decl) loop
-            if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
-               Spec := Specification (Original_Node (Decl));
-               Sent := Defining_Unit_Name (Spec);
-               Prag := Spec_PPC_List (Sent);
-               while Present (Prag) loop
-                  Analyze_PPC_In_Decl_Part (Prag, Sent);
-                  Prag := Next_Pragma (Prag);
-               end loop;
-            end if;
-
-            Next (Decl);
-         end loop;
-      end Analyze_PPCs;
-
       ---------------------
       -- Clear_Constants --
       ---------------------
@@ -1161,7 +1127,6 @@  package body Sem_Ch7 is
    begin
       if Present (Vis_Decls) then
          Analyze_Declarations (Vis_Decls);
-         Analyze_PPCs (Vis_Decls);
       end if;
 
       --  Verify that incomplete types have received full declarations
@@ -1296,7 +1261,6 @@  package body Sem_Ch7 is
          end if;
 
          Analyze_Declarations (Priv_Decls);
-         Analyze_PPCs (Priv_Decls);
 
          --  Check the private declarations for incomplete deferred constants
 
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 165610)
+++ einfo.adb	(working copy)
@@ -2581,7 +2581,10 @@  package body Einfo is
 
    function Spec_PPC_List (Id : E) return N is
    begin
-      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+      pragma Assert
+        (Ekind (Id) = E_Entry
+          or else Is_Subprogram (Id)
+          or else Is_Generic_Subprogram (Id));
       return Node24 (Id);
    end Spec_PPC_List;
 
@@ -5046,7 +5049,10 @@  package body Einfo is
 
    procedure Set_Spec_PPC_List (Id : E; V : N) is
    begin
-      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+      pragma Assert
+        (Ekind_In (Id, E_Entry, E_Void)
+          or else Is_Subprogram (Id)
+          or else Is_Generic_Subprogram (Id));
       Set_Node24 (Id, V);
    end Set_Spec_PPC_List;
 
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 165610)
+++ einfo.ads	(working copy)
@@ -3532,11 +3532,12 @@  package Einfo is
 --       the corresponding parameter entities in the spec.
 
 --    Spec_PPC_List (Node24)
---       Present in subprogram and generic subprogram entities. Points to a
---       list of Precondition and Postcondition pragma nodes for preconditions
---       and postconditions declared in the spec. The last pragma encountered
---       is at the head of this list, so it is in reverse order of textual
---       appearance.
+--       Present in entries, and in subprogram and generic subprogram entities.
+--       Points to a list of Precondition and Postcondition pragma nodes for
+--       preconditions and postconditions declared in the spec. The last pragma
+--       encountered is at the head of this list, so it is in reverse order of
+--       textual appearance. Note that this includes precondition/postcondition
+--       pragmas generated to correspond to Pre/Post aspects.
 
 --    Storage_Size_Variable (Node15) [implementation base type only]
 --       Present in access types and task type entities. This flag is set
@@ -4951,6 +4952,7 @@  package Einfo is
    --    Accept_Address                      (Elist21)
    --    Scope_Depth_Value                   (Uint22)
    --    Protection_Object                   (Node23)   (protected kind)
+   --    Spec_PPC_List                       (Node24)   (for entry only)
    --    Default_Expressions_Processed       (Flag108)
    --    Entry_Accepted                      (Flag152)
    --    Is_AST_Entry                        (Flag132)  (for entry only)
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 165610)
+++ sem_prag.adb	(working copy)
@@ -240,9 +240,7 @@  package body Sem_Prag is
    ------------------------------
 
    procedure Analyze_PPC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
-      Arg1 : constant Node_Id :=
-               First (Pragma_Argument_Associations (N));
-      Arg2 : constant Node_Id := Next (Arg1);
+      Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
 
    begin
       --  Install formals and push subprogram spec onto scope stack so that we
@@ -257,13 +255,6 @@  package body Sem_Prag is
       Preanalyze_Spec_Expression
         (Get_Pragma_Arg (Arg1), Standard_Boolean);
 
-      --  If there is a message argument, analyze it the same way
-
-      if Present (Arg2) then
-         Preanalyze_Spec_Expression
-           (Get_Pragma_Arg (Arg2), Standard_String);
-      end if;
-
       --  Remove the subprogram from the scope stack now that the pre-analysis
       --  of the precondition/postcondition is done.
 
@@ -1511,8 +1502,7 @@  package body Sem_Prag is
                     ("pragma% cannot be applied to abstract subprogram");
 
                elsif Class_Present (N) then
-                  Error_Pragma
-                    ("aspect `%''Class` not implemented yet");
+                  null;
 
                else
                   Error_Pragma
@@ -1520,14 +1510,19 @@  package body Sem_Prag is
                end if;
 
             elsif not Nkind_In (PO, N_Subprogram_Declaration,
-                                    N_Generic_Subprogram_Declaration)
+                                    N_Generic_Subprogram_Declaration,
+                                    N_Entry_Declaration)
             then
                Pragma_Misplaced;
             end if;
 
-            --  Here if we have subprogram or generic subprogram declaration
+            --  Here if we have [generic] subprogram or entry declaration
 
-            S := Defining_Unit_Name (Specification (PO));
+            if Nkind (PO) = N_Entry_Declaration then
+               S := Defining_Entity (PO);
+            else
+               S := Defining_Unit_Name (Specification (PO));
+            end if;
 
             --  Make sure we do not have the case of a precondition pragma when
             --  the Pre'Class aspect is present.
@@ -1583,14 +1578,11 @@  package body Sem_Prag is
                end;
             end if;
 
-            --  Analyze the pragma unless it appears within a package spec,
-            --  which is the case where we delay the analysis of the PPC until
-            --  the end of the package declarations (for details, see
-            --  Analyze_Package_Specification.Analyze_PPCs).
-
-            if not Is_Package_Or_Generic_Package (Scope (S)) then
-               Analyze_PPC_In_Decl_Part (N, S);
-            end if;
+            --  Note: we do not analye the pragma at this point. Instead we
+            --  delay this analysis until the end of the declarative part in
+            --  which the pragma appears. This implements the required delay
+            --  in this analysis, allowing forward references. The analysis
+            --  happens at the end of Analyze_Declarations.
 
             --  Chain spec PPC pragma to list for subprogram
 
@@ -1610,6 +1602,15 @@  package body Sem_Prag is
             Pragma_Misplaced;
          end if;
 
+         --  Preanalyze message argument if present. Visibility in this
+         --  argument is established at the point of pragma occurrence.
+
+         if Arg_Count = 2 then
+            Check_Optional_Identifier (Arg2, Name_Message);
+            Preanalyze_Spec_Expression
+              (Get_Pragma_Arg (Arg2), Standard_String);
+         end if;
+
          --  Record if pragma is enabled
 
          if Check_Enabled (Pname) then
@@ -10823,7 +10824,6 @@  package body Sem_Prag is
             Check_At_Least_N_Arguments (1);
             Check_At_Most_N_Arguments (2);
             Check_Optional_Identifier (Arg1, Name_Check);
-
             Check_Precondition_Postcondition (In_Body);
 
             --  If in spec, nothing more to do. If in body, then we convert the
@@ -10833,11 +10833,6 @@  package body Sem_Prag is
             --  analyze the condition itself in the proper context.
 
             if In_Body then
-               if Arg_Count = 2 then
-                  Check_Optional_Identifier (Arg3, Name_Message);
-                  Analyze_And_Resolve (Get_Pragma_Arg (Arg2), Standard_String);
-               end if;
-
                Rewrite (N,
                  Make_Pragma (Loc,
                    Chars => Name_Check,
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 165610)
+++ sem_ch6.adb	(working copy)
@@ -8699,18 +8699,22 @@  package body Sem_Ch6 is
          --  do this fiddling, for the spec cases, the already preanalyzed
          --  parameters are not affected.
 
+         Set_Analyzed (CP, False);
+
+         --  We also make sure Comes_From_Source is False for the copy
+
+         Set_Comes_From_Source (CP, False);
+
          --  For a postcondition pragma within a generic, preserve the pragma
          --  for later expansion.
 
-         Set_Analyzed (CP, False);
-
          if Nam = Name_Postcondition
            and then not Expander_Active
          then
             return CP;
          end if;
 
-         --  Change pragma into corresponding pragma Check
+         --  Change copy of pragma into corresponding pragma Check
 
          Prepend_To (Pragma_Argument_Associations (CP),
            Make_Pragma_Argument_Association (Sloc (Prag),
@@ -8761,9 +8765,8 @@  package body Sem_Ch6 is
 
          Prag := Spec_PPC_List (Spec_Id);
          while Present (Prag) loop
-            if Pragma_Name (Prag) = Name_Precondition
-              and then Pragma_Enabled (Prag)
-            then
+            if Pragma_Name (Prag) = Name_Precondition then
+
                --  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
@@ -8969,7 +8972,6 @@  package body Sem_Ch6 is
                Prag := Spec_PPC_List (Spec);
                loop
                   if Pragma_Name (Prag) = Name_Postcondition
-                    and then Pragma_Enabled (Prag)
                     and then (not Class or else Class_Present (Prag))
                   then
                      if Plist = No_List then
Index: sem_disp.adb
===================================================================
--- sem_disp.adb	(revision 165610)
+++ sem_disp.adb	(working copy)
@@ -1742,8 +1742,29 @@  package body Sem_Disp is
       Parent_Op : Entity_Id;
       --  Traverses the Overridden_Operation chain
 
+      procedure Store_IS (E : Entity_Id);
+      --  Stores E in Result if not already stored
+
+      --------------
+      -- Store_IS --
+      --------------
+
+      procedure Store_IS (E : Entity_Id) is
+      begin
+         for J in 1 .. N loop
+            if E = Result (J) then
+               return;
+            end if;
+         end loop;
+
+         N := N + 1;
+         Result (N) := E;
+      end Store_IS;
+
+   --  Start of processing for Inherited_Subprograms
+
    begin
-      if Present (S) then
+      if Present (S) and then Is_Dispatching_Operation (S) then
 
          --  Deal with direct inheritance
 
@@ -1755,13 +1776,56 @@  package body Sem_Disp is
             if Is_Subprogram (Parent_Op)
               or else Is_Generic_Subprogram (Parent_Op)
             then
-               N := N + 1;
-               Result (N) := Parent_Op;
+               Store_IS (Parent_Op);
             end if;
          end loop;
 
-         --  For now don't bother with interfaces, TBD ???
+         --  Now deal with interfaces
+
+         declare
+            Tag_Typ : Entity_Id;
+            Prim    : Entity_Id;
+            Elmt    : Elmt_Id;
+
+         begin
+            Tag_Typ := Find_Dispatching_Type (S);
+
+            if Is_Concurrent_Type (Tag_Typ) then
+               Tag_Typ := Corresponding_Record_Type (Tag_Typ);
+            end if;
 
+            --  Search primitive operations of dispatching type
+
+            if Present (Tag_Typ)
+              and then Present (Primitive_Operations (Tag_Typ))
+            then
+               Elmt := First_Elmt (Primitive_Operations (Tag_Typ));
+               while Present (Elmt) loop
+                  Prim := Node (Elmt);
+
+                  --  The following test eliminates some odd cases in which
+                  --  Ekind (Prim) is Void, to be investigated further ???
+
+                  if not (Is_Subprogram (Prim)
+                            or else
+                          Is_Generic_Subprogram (Prim))
+                  then
+                     null;
+
+                     --  For [generic] subprogram, look at interface alias
+
+                  elsif Present (Interface_Alias (Prim))
+                    and then Alias (Prim) = S
+                  then
+                     --  We have found a primitive covered by S
+
+                     Store_IS (Interface_Alias (Prim));
+                  end if;
+
+                  Next_Elmt (Elmt);
+               end loop;
+            end if;
+         end;
       end if;
 
       return Result (1 .. N);