Patchwork [Ada] Implementation of Ada 2012 type invariants

login
register
mail settings
Submitter Arnaud Charlet
Date Sept. 6, 2011, 9:33 a.m.
Message ID <20110906093313.GA30757@adacore.com>
Download mbox | patch
Permalink /patch/113518/
State New
Headers show

Comments

Arnaud Charlet - Sept. 6, 2011, 9:33 a.m.
The final version of the Ada 2012 RM specifies that a type invariant can be
given in the private part of a package, on the completion of a private type
declaration.
The following must compile quietly:

package Inv is
   type List is private;
private
   type Length_T is new Integer;
   type Array_T is array (Length_T range <>) of Integer;
   type Array_Ptr_T is access Array_T;
   type List is record
      Length : Length_T;
      Item   : Array_Ptr_T;
   end record
     with Type_Invariant =>
       List.Item'First = 1 and List.Item'Last = List.Length;
end Inv;

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

2011-09-06  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Analyze_Pragma, case Type_Invariant): A type invariant
	is allowed on a full type declaration if it is the completion of
	a private declarations.
	* sem_ch13.adb (Analyze_Aspect_Specifications): An invariant
	aspect is allowed on a full type declaration in the private part
	of a package.

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 178565)
+++ sem_prag.adb	(working copy)
@@ -10088,10 +10088,21 @@ 
             if Typ = Any_Type then
                return;
 
-            elsif not Ekind_In (Typ, E_Private_Type,
+            --  An invariant must apply to a private type, or appear in the
+            --  private part of a package spec and apply to a completion.
+
+            elsif Ekind_In (Typ, E_Private_Type,
                                      E_Record_Type_With_Private,
                                      E_Limited_Private_Type)
             then
+               null;
+
+            elsif In_Private_Part (Current_Scope)
+              and then Has_Private_Declaration (Typ)
+            then
+               null;
+
+            else
                Error_Pragma_Arg
                  ("pragma% only allowed for private type", Arg1);
             end if;
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 178565)
+++ sem_ch13.adb	(working copy)
@@ -1289,11 +1289,22 @@ 
                when Aspect_Invariant      |
                     Aspect_Type_Invariant =>
 
-                  --  Check placement legality
+                  --  Check placement legality: An invariant must apply to a
+                  --  private type, or appear in the private part of a spec.
+                  --  Analysis of the pragma will verify that in the private
+                  --  part it applies to a completion.
 
-                  if not Nkind_In (N, N_Private_Type_Declaration,
+                  if Nkind_In (N, N_Private_Type_Declaration,
                                       N_Private_Extension_Declaration)
                   then
+                     null;
+
+                  elsif Nkind (N) = N_Full_Type_Declaration
+                    and then In_Private_Part (Current_Scope)
+                  then
+                     null;
+
+                  else
                      Error_Msg_N
                        ("invariant aspect must apply to a private type", N);
                   end if;