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

[Arnaud Charlet <charlet at adacore dot com>]

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.

Attachment: difs
Description: Text document