[Ada] Implement Invariant aspect and pragma

This patch implements the Invariant aspect, from AI AI05-0146-1/04.
The implementation is complete except that inheritance of aspects
from interfaces is not yet done. Inheritance of Invariant'Class for
the normal case of derived tagged types does work. An Invariant
pragma has also been introduced, allowing use of this facility
in earlier versions of Ada (before Ada 2012).

The following test is for the Invariant aspect (non-inherited case)

     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 Simpleinv is
     5.    package X is
     6.       type R is private with
     7.          Invariant => 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 with
    13.         Invariant => 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 Simpleinv;

The output when compiled with -gnata12 is:

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

The following test is for Invariant'Class showing
inheritance and proper dispatching. This is compiled
with -gnata12 -gnatj60

     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 Inheritinv is
     5.    package X is
     6.
     7.       type T1 is tagged private with
     8.         Invariant'Class => Testt1 (T1);
     9.
    10.       function Testt1 (X : T1) return Boolean;
    11.       function Maket1 return T1;
    12.
    13.       type T2 is new T1 with private;
    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
                   |
        >>> info: "T2" inherits "Invariant'Class" aspect
            from line 8

    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 Inheritinv;

The output is:

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

The following checks

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

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

	* atree.h (Field29): Fix incorrect definition.
	* einfo.adb (Invariant_Procedure): New attribute
	(Has_Invariants): New flag
	(Has_Inheritable_Invariants): New flag
	(OK_To_Reference): New flag
	Minor code reorganization (use Next_Rep_Item function)
	* einfo.ads (Invariant_Procedure): New attribute
	(Has_Invariants): New flag
	(Has_Inheritable_Invariants): New flag
	(OK_To_Reference): New flag
	* exp_ch3.adb (Expand_N_Object_Declaration): Add check for invariant
	* exp_ch4.adb (Expand_N_Type_Conversion): Check invariant on type
	conversion.  Minor reformatting.
	* exp_util.ads, exp_util.adb (Make_Invariant_Call): New procedure.
	* opt.ads (List_Inherited_Aspects): New name for List_Inherited_Pre_Post
	* par-prag.adb: Add dummy entry for pragma Invariant.
	* sem_ch13.adb (Build_Invariant_Procedure): New procedure
	(Analyze_Aspect_Specification): Add support for Invariant aspect
	* sem_ch13.ads (Build_Invariant_Procedure): New procedure
	* sem_ch3.adb (Build_Derived_Type): Propagate invariant information
	(Process_Full_View): Deal with invariants, building invariant procedure
	Minor reformatting
	* sem_ch6.adb (Process_PPCs): Add processing of invariants
	* sem_ch7.adb (Analyze_Package_Specification): Build invariant
	procedures.
	* sem_prag.adb: Implement pragma Invariant.
	* sem_res.adb (Resolve_Entity_Name): Allow type reference if
	OK_To_Reference set.
	* sem_warn.adb (List_Inherited_Aspects): New name for
	List_Inherited_Pre_Post.
	* snames.ads-tmpl: Add entries for pragma Invariant.
	* treepr.adb (Print_Entity_Information): Add handling of Field29.
	* usage.adb: Warning .l/.L applies to invariant as well as pre/post.

[Ada] Implement Invariant aspect and pragma

Commit Message

Patch