[Ada] Implement pragmas Type_Invariant[_Class]

[Arnaud Charlet <charlet at adacore dot com>]

This implements two new pragmas, whose names, syntax, and semantics
match the corresponding aspects Type_Invariant and Type_Invariant'Class
as closely as possible. For Type_Invariant'Class the pragma is named
Type_Invariant_Class, since the attribute form of the name is not legal
for a pragma name.

The following test

     1. with Ada.Text_IO;    use Ada.Text_IO;
     2. with Ada.Assertions; use Ada.Assertions;
     3. with Ada.Exceptions; use Ada.Exceptions;
     4. procedure PSimpleinv is
     5.    package X is
     6.       type R is private;
     7.       pragma Type_Invariant (R, Testr (R));
     8.       function Testr (X : R) return Boolean;
     9.       function Gen (X : Integer) return R;
    10.       procedure Make (X : out R);
    11.
    12.       type T1 is tagged private;
    13.       pragma Type_Invariant (T1, Testt1 (T1));
    14.       type T2 is new T1 with private;
    15.       function Testt1 (X : T1) return Boolean;
    16.       function Maket2 return T2;
    17.
    18.    private
    19.       type R is record
    20.          Field : Integer := 4;
    21.       end record;
    22.
    23.       type T1 is tagged record
    24.          Field : Integer := 4;
    25.       end record;
    26.
    27.       type T2 is new T1 with record
    28.          Field2 : Integer := 4;
    29.       end record;
    30.    end X;
    31.
    32.    package body X is
    33.       function Testr (X : R) return Boolean is
    34.       begin
    35.          return X.Field mod 2 = 1;
    36.       end Testr;
    37.
    38.       function Gen (X : Integer) return R is
    39.       begin
    40.          return (Field => X);
    41.       end Gen;
    42.
    43.       procedure Make (X : out R) is
    44.       begin
    45.          X := (Field => 4);
    46.       end Make;
    47.
    48.       function Testt1 (X : T1) return Boolean is
    49.       begin
    50.          return X.Field mod 2 = 1;
    51.       end Testt1;
    52.
    53.       function Maket2 return T2 is
    54.       begin
    55.          return (Field => 4, Field2 => 3);
    56.       end Maket2;
    57.
    58.       --  No exception, private initialization
    59.
    60.       VPrivate : R := (Field => 6);
    61.    end X;
    62.
    63. begin
    64.    --  No exception, OK initialization
    65.
    66.    begin
    67.       declare
    68.          V1 : X.R := X.Gen (5);
    69.       begin
    70.          null;
    71.       end;
    72.       Put_Line ("V1: no exception");
    73.    end;
    74.
    75.    --  Bad result from public function
    76.
    77.    begin
    78.       declare
    79.          V2 : X.R := X.Gen (4);
    80.       begin
    81.          null;
    82.       end;
    83.       Put_Line ("V2: no exception");
    84.    exception
    85.       when E : Assertion_Error =>
    86.          Put_Line ("V2: " & Exception_Message (E));
    87.    end;
    88.
    89.    --  Bad default initialization
    90.
    91.    begin
    92.       declare
    93.          V3 : X.R;
    94.       begin
    95.          null;
    96.       end;
    97.       Put_Line ("V3: no exception");
    98.    exception
    99.       when E : Assertion_Error =>
   100.          Put_Line ("V3: " & Exception_Message (E));
   101.    end;
   102.
   103.    --  Bad OUT parameter
   104.
   105.    begin
   106.       declare
   107.          V4 : X.R := X.Gen (5);
   108.       begin
   109.          X.Make (V4);
   110.       end;
   111.       Put_Line ("V4: no exception");
   112.    exception
   113.       when E : Assertion_Error =>
   114.          Put_Line ("V4: " & Exception_Message (E));
   115.    end;
   116.
   117.    --  Bad conversion
   118.
   119.    begin
   120.       declare
   121.          TT : X.T2 := X.Maket2;
   122.          V5 : X.T1 := X.T1 (TT);
   123.       begin
   124.          null;
   125.       end;
   126.       Put_Line ("V5: no exception");
   127.    exception
   128.       when E : Assertion_Error =>
   129.          Put_Line ("V5: " & Exception_Message (E));
   130.    end;
   131. end PSimpleinv;

compiled with -gnata12 -gnatw.l, outputs:

V1: no exception
V2: failed invariant from psimpleinv.adb:7
V3: failed invariant from psimpleinv.adb:7
V4: failed invariant from psimpleinv.adb:7
V5: failed invariant from psimpleinv.adb:13

The following test:

     1. with Ada.Text_IO;    use Ada.Text_IO;
     2. with Ada.Assertions; use Ada.Assertions;
     3. with Ada.Exceptions; use Ada.Exceptions;
     4. procedure PInheritinv is
     5.    package X is
     6.
     7.       type T1 is tagged private;
     8.       pragma Type_Invariant_Class (T1, Testt1 (T1));
     9.
    10.       function Testt1 (X : T1) return Boolean;
    11.       function Maket1 return T1;
    12.
    13.       type T2 is new T1 with private;
                   |
        >>> info: "T2" inherits "Invariant'Class" aspect from line 8

    14.
    15.       function Maket2 return T2;
    16.       function Testt1 (X : T2) return Boolean;
    17.       function Maket1 return T2;
    18.
    19.    private
    20.       type T1 is tagged record
    21.          Field1 : Integer := 4;
    22.       end record;
    23.
    24.       type T2 is new T1 with record
    25.          Field2 : Integer := 4;
    26.       end record;
    27.    end X;
    28.
    29.    package body X is
    30.
    31.       function Testt1 (X : T1) return Boolean is
    32.       begin
    33.          return X.Field1 mod 2 = 1;
    34.       end Testt1;
    35.
    36.       function Testt1 (X : T2) return Boolean is
    37.       begin
    38.          return X.Field1 mod 2 = 0;
    39.       end Testt1;
    40.
    41.       function Maket1 return T1 is
    42.       begin
    43.          return (Field1 => 4);
    44.       end Maket1;
    45.
    46.       function Maket1 return T2 is
    47.       begin
    48.          return (Field1 => 4, Field2 => 3);
    49.       end Maket1;
    50.
    51.       function Maket2 return T2 is
    52.       begin
    53.          return (Field1 => 5, Field2 => 3);
    54.       end Maket2;
    55.    end X;
    56.
    57. begin
    58.    --  Bad value from Maket1
    59.
    60.    begin
    61.       declare
    62.          V1 : X.T1 := X.Maket1;
    63.       begin
    64.          null;
    65.       end;
    66.       Put_Line ("V1: no exception");
    67.    exception
    68.       when E : Assertion_Error =>
    69.          Put_Line ("V1: " & Exception_Message (E));
    70.    end;
    71.
    72.    --  Bad value from Maket2
    73.    --  (tested with overridden testt1)
    74.
    75.    begin
    76.       declare
    77.          V2 : X.T2 := X.Maket2;
    78.       begin
    79.          null;
    80.       end;
    81.       Put_Line ("V2: no exception");
    82.    exception
    83.       when E : Assertion_Error =>
    84.          Put_Line ("V2: " & Exception_Message (E));
    85.    end;
    86.
    87.    --  OK value from overridden Maket1
    88.    --  (tested with overridden testt1)
    89.
    90.    begin
    91.       declare
    92.          V3 : X.T2 := X.Maket1;
    93.       begin
    94.          null;
    95.       end;
    96.       Put_Line ("V3: no exception");
    97.    exception
    98.       when E : Assertion_Error =>
    99.          Put_Line ("V3: " & Exception_Message (E));
   100.    end;
   101.
   102. end PInheritinv;

compiled with -gnata12 -gnatw.l, outputs:

V1: failed invariant from pinheritinv.adb:8
V2: failed invariant from pinheritinv.adb:8
V3: no exception

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

2013-10-14  Robert Dewar  <dewar@adacore.com>

	* exp_prag.adb (Expand_Pragma_Check): Generate proper string
	for invariant
	* gnat_rm.texi: Add documentation for pragmas
	Type_Invariant[_Class]
	* par-prag.adb: Add entries for pragmas Type_Invariant[_Class]
	* sem_ch13.adb: Minor reformatting
	* sem_prag.adb: Implement pragmas Type_Invariant[_Class]
	* snames.ads-tmpl: Add entries for pragmas Type_Invariant[_Class]

Attachment: difs
Description: Text document