[Ada] Final fix to inheriting of Pre'Class preconditions

[Arnaud Charlet <charlet at adacore dot com>]

With this patch, the inheritance of Pre'Class preconditions with
the resulting composite condition formed by linking the inherited
expressions with OR ELSE is working.

Still to do

a) deal with visibility issue, GNAT currently only delays pre/post
analysis in the package case, the RM does it in all declarative
units.

b) deal with interfaces

c) deal with entries

Here is the latest status of the test programs

Testing for errors:
(compiled with -gnata12 -gnatld7 -gnatj60)

     1. package Preposterr is
     2.    procedure P0 is abstract with
     3.      Pre  => True,
             |
        >>> aspect "Pre" requires 'Class for abstract
            subprogram

     4.      Post => False;
             |
        >>> aspect "Post" requires 'Class for abstract
            subprogram

     5.
     6.    procedure P1 is abstract;
     7.    pragma Precondition (True);
           |
        >>> pragma "Precondition" cannot be applied to
            abstract subprogram

     8.    pragma Postcondition (False);
           |
        >>> pragma "Postcondition" cannot be applied to
            abstract subprogram

     9.
    10.    procedure P2 with
    11.      Pre  => True,
    12.      Post => False;
    13.    pragma Precondition (True);
    14.    pragma Postcondition (False);
    15.
    16.    procedure P3 with
    17.      Pre'Class  => True,
    18.      Post'Class => False;
    19.    pragma Precondition (True);
           |
        >>> pragma "Precondition" not allowed, "Pre'Class"
            aspect given at line 17

    20.    pragma Postcondition (False);
    21.
    22.    procedure P4 with
    23.      Pre       => True,
    24.      Pre'Class => True;
             |
        >>> aspect "Pre'Class" for "P4" is not allowed
            here, since aspect "Pre" previously given at
            line 23

    25.
    26.    procedure P5 with
    27.      Pre'Class => True,
    28.      Pre       => True;
             |
        >>> aspect "Pre" for "P5" is not allowed here,
            since aspect "Pre'Class" previously given at
            line 27

    29.
    30.    procedure P6 with
    31.      Pre       => True,
    32.      Pre       => True;
             |
        >>> aspect "Pre" for "P6" previously given at line
            31

    33.
    34.    procedure P7 with
    35.      Pre'Class => True,
    36.      Pre'Class => True;
             |
        >>> aspect "Pre'Class" for "P7" previously given at
            line 35

    37.
    38.    procedure P8 with
    39.      Post       => True,
    40.      Post'Class => True;
    41.
    42.    procedure P9 with
    43.      Post'Class => True,
    44.      Post       => True;
    45.
    46.    procedure P10 with
    47.      Post       => True,
    48.      Post       => True;
             |
        >>> aspect "Post" for "P10" previously given at
            line 47

    49.
    50.    procedure P11 with
    51.      Post'Class => True,
    52.      Post'Class => True;
             |
        >>> aspect "Post'Class" for "P11" previously given
            at line 51

    53.
    54.    type T is tagged null record;
    55.    procedure PT (Arg : T) with
    56.      Pre'Class => True;
    57.
    58.    type NT is new T with null record;
    59.    procedure PT (Arg : NT) with
                     |
        >>> info: "PT" inherits "Pre'Class" aspect from
            line 56

    60.      Pre => True;
             |
        >>> aspect "Pre" not allowed, "Pre'Class" aspect
            inherited from line 56

    61. end Preposterr;

Testing non-inherited pre/postconditions
compiled with -gnata12 -gnatld7

     1. with Text_IO; use Text_IO;
     2. with Ada.Exceptions; use Ada.Exceptions;
     3. procedure prepost is
     4.    function F (X : Integer) return Integer with
     5.    Pre  =>
     6.      X > 11
     7.        and then
     8.      X mod 2 = 1,
     9.    Post =>
    10.      F'Result = X + 1
    11.        and then
    12.      F'Result /= 18;
    13.
    14.    function F (X : Integer) return Integer is
    15.    begin
    16.       if X = 13 then
    17.          return X;
    18.       else
    19.          return X + 1;
    20.       end if;
    21.    end F;
    22.
    23.
    24. begin
    25.    Put_Line (F (31)'Img);
    26.
    27.    begin
    28.       Put_Line (F (13)'Img);
    29.    exception
    30.       when E : others =>
    31.          Put_Line ("exception for F (13): "
    32.                    & Exception_Message (E));
    33.    end;
    34.
    35.    begin
    36.       Put_Line (F (12)'Img);
    37.    exception
    38.       when E : others =>
    39.          Put_Line ("exception for F (12): "
    40.                    & Exception_Message (E));
    41.    end;
    42.
    43.    begin
    44.       Put_Line (F (11)'Img);
    45.    exception
    46.       when E : others =>
    47.          Put_Line ("exception for F (11): "
    48.                    & Exception_Message (E));
    49.    end;
    50.
    51.    begin
    52.       Put_Line (F (17)'Img);
    53.    exception
    54.       when E : others =>
    55.          Put_Line ("exception for F (17): "
    56.                    & Exception_Message (E));
    57.    end;
    58. end prepost;

The output is:

 32
exception for F (13): failed postcondition from prepost.adb:10
exception for F (12): failed precondition from prepost.adb:8
exception for F (11): failed precondition from prepost.adb:6
exception for F (17): failed postcondition from prepost.adb:12

If gnat.adc contains pragma Suppress_Exception_Locations, then
the output is:

 32
exception for F (13):
exception for F (12):
exception for F (11):
exception for F (17):

Testing for inherited pre/post conditions:
(compiled with -gnata12-gnatld7)

     1. with Text_IO; use Text_IO;
     2. with Ada.Exceptions; use Ada.Exceptions;
     3. procedure PrePostI is
     4.    function Ident (X : Integer) return Integer is
     5.    begin
     6.       return X;
     7.    end;
     8.
     9.    package Ops is
    10.       G : Integer := Ident (13);
    11.
    12.       type R is tagged record
    13.          X : Integer;
    14.       end record;
    15.
    16.       procedure RP (Arg : in out R) with
    17.         Post'Class =>
    18.           Arg.X = Arg.X'Old + 1
    19.             and then
    20.           Arg.X /= G,
    21.         Pre'Class =>
    22.           Arg.X = 99 or else Arg.X = 12;
    23.    end Ops;
    24.
    25.    package Ops2 is
    26.       G : Integer := Ident (999);
    27.
    28.       type RN is new Ops.R with record
    29.          Y : Integer;
    30.       end record;
    31.
    32.       procedure RP (Arg : in out RN) with
                        |
        >>> info: "RP" inherits "Post'Class" aspect from line 17
        >>> info: "RP" inherits "Pre'Class" aspect from line 21

    33.         Post =>
    34.           Arg.Y = Incr (Arg.Y'Old)
    35.             and then
    36.           Arg.Y /= 11,
    37.         Pre'Class =>
    38.           Arg.Y = 10
    39.             or else
    40.           Arg.Y = 99
    41.             or else
    42.           Arg.Y = 77;
    43.       function Incr (Arg : Integer) return Integer;
    44.    end Ops2;
    45.
    46.    package body Ops is
    47.       procedure RP (Arg : in out R) is
    48.       begin
    49.          null;
    50.       end;
    51.    end Ops;
    52.
    53.    package body Ops2 is
    54.       procedure RP (Arg : in out RN) is
    55.       begin
    56.          if Arg.X /= 99 then
    57.             Arg.X := Arg.X + 1;
    58.          end if;
    59.
    60.          if Arg.Y /= 99 then
    61.             Arg.Y := Arg.Y + 1;
    62.          end if;
    63.       end RP;
    64.
    65.       function Incr (Arg : Integer) return Integer is
    66.       begin
    67.          return Arg + 1;
    68.       end Incr;
    69.    end Ops2;
    70.
    71.    use Ops, Ops2;
    72.
    73.    V : RN;
    74.
    75. begin
    76.    V.X := 63;
    77.    V.Y := 77;
    78.    RP (V);
    79.    Put_Line ("V.X =" & V.X'Img);
    80.    Put_Line ("V.Y =" & V.Y'Img);
    81.
    82.    begin
    83.       V.X := 99;
    84.       V.Y := 72;
    85.       RP (V);
    86.       Put_Line ("RP (99,72), no exception");
    87.    exception
    88.       when E : others =>
    89.          New_Line;
    90.          Put_Line ("exception for RP ((99,72))):");
    91.          Put_Line ("  " & Exception_Message (E));
    92.    end;
    93.
    94.    begin
    95.       V.X := 12;
    96.       V.Y := 72;
    97.       RP (V);
    98.       Put_Line ("RP (12,72), no exception");
    99.    exception
   100.       when E : others =>
   101.          New_Line;
   102.          Put_Line ("exception for RP ((12,72))):");
   103.          Put_Line ("  " & Exception_Message (E));
   104.    end;
   105.
   106.    begin
   107.       V.X := 52;
   108.       V.Y := 10;
   109.       RP (V);
   110.       Put_Line ("RP (52,10), no exception");
   111.    exception
   112.       when E : others =>
   113.          New_Line;
   114.          Put_Line ("exception for RP ((52,10))): ");
   115.          Put_Line ("  " & Exception_Message (E));
   116.    end;
   117.
   118.    begin
   119.       V.X := 23;
   120.       V.Y := 99;
   121.       RP (V);
   122.       Put_Line ("RP (23,99), no exception");
   123.    exception
   124.       when E : others =>
   125.          New_Line;
   126.          Put_Line ("exception for RP ((23,99))): ");
   127.          Put_Line ("  " & Exception_Message (E));
   128.    end;
   129.
   130.    begin
   131.       V.X := 24;
   132.       V.Y := 99;
   133.       RP (V);
   134.       Put_Line ("RP (24,99), no exception");
   135.    exception
   136.       when E : others =>
   137.          New_Line;
   138.          Put_Line ("exception for RP ((24,99))): ");
   139.          Put_Line ("  " & Exception_Message (E));
   140.    end;
   141.
   142.    begin
   143.       V.X := 23;
   144.       V.Y := 98;
   145.       RP (V);
   146.       Put_Line ("RP (23,98), no exception");
   147.    exception
   148.       when E : others =>
   149.          New_Line;
   150.          Put_Line ("exception for RP ((23,98))): ");
   151.          Put_Line ("  " & Exception_Message (E));
   152.    end;
   153. end PrePostI;

The output is:

V.X = 64
V.Y = 78

exception for RP ((99,72))):
  failed inherited postcondition from preposti.adb:18

exception for RP ((12,72))):
  failed inherited postcondition from preposti.adb:20

exception for RP ((52,10))):
  failed postcondition from preposti.adb:36

exception for RP ((23,99))):
  failed postcondition from preposti.adb:34

exception for RP ((24,99))):
  failed postcondition from preposti.adb:34

exception for RP ((23,98))):
  failed precondition from preposti.adb:41
  also failed inherited precondition from preposti.adb:22

If gnat.adc contains pragma Suppress_Exception_Locations, then
the output is:

V.X = 64
V.Y = 78

exception for RP ((99,72))):


exception for RP ((12,72))):


exception for RP ((52,10))):


exception for RP ((23,99))):


exception for RP ((24,99))):


exception for RP ((23,98))):

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

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

	* sem_ch6.adb (Process_PPCs): Fix error in inheriting Pre'Class when no
	exception messages are generated.
	(Process_PPCs): Fix error in inheriting Pre'Class.

Attachment: difs
Description: Text document