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 <schonb...@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.
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;