This patch fixes the handling of type invariants when they are specified on the completion of a private type, and when public expression functions return a type with invariants.
Running the following: gnatmake -q -gnat12a main main must yield: OK --- with Ada.Assertions; use Ada.Assertions; with Text_IO; use Text_IO; with R; use R; procedure Main is X : T; begin X := Zero; Put_Line ("Invariant violated"); exception when Assertion_Error => Put_Line ("OK"); end Main; --- package R is type T is private;; function Non_Null (X : T) return Boolean; function Zero return T; private type T is new Integer with Type_Invariant => T /= 0; function Non_Null (X : T) return Boolean is (X /= 0); function Zero return T is (0); end R; Tested on x86_64-pc-linux-gnu, committed on trunk 2012-10-05 Ed Schonberg <schonb...@adacore.com> * einfo.adb (Set_Invariant_Procedure, Set_Predicate_Function): chain properly subprograms on Subprograms_For_Type list. * sem_ch13.ads; (Build_Invariant_Procedure_Declaration): new procedure, to create declaration for invariant procedure independently of the construction of the body, so that it can be called within expression functions. * sem_ch13.adb (Build_Invariant_Procedure): code cleanup. The declaration may already have been generated at the point an explicit invariant aspect is encountered. * sem_prag.adb; (Analyze_Pragma, case Invariant): create declaration for invariant procedure. * sem_ch7.adb (Analyze_Package_Specification): clean up call to build invariant procedure. (Preserve_Full_Attributes): propagate information about invariants if they appear on a completion,
Index: sem_ch7.adb =================================================================== --- sem_ch7.adb (revision 192066) +++ sem_ch7.adb (working copy) @@ -28,6 +28,7 @@ -- handling of private and full declarations, and the construction of dispatch -- tables for tagged types. +with Aspects; use Aspects; with Atree; use Atree; with Debug; use Debug; with Einfo; use Einfo; @@ -1387,7 +1388,21 @@ and then Nkind (Parent (E)) = N_Full_Type_Declaration and then Has_Aspects (Parent (E)) then - Build_Invariant_Procedure (E, N); + declare + ASN : Node_Id; + begin + ASN := First (Aspect_Specifications (Parent (E))); + while Present (ASN) loop + if Chars (Identifier (ASN)) = Name_Invariant + or else Chars (Identifier (ASN)) = Name_Type_Invariant + then + Build_Invariant_Procedure (E, N); + exit; + end if; + + Next (ASN); + end loop; + end; end if; Next_Entity (E); @@ -2143,6 +2158,14 @@ Set_Freeze_Node (Priv, Freeze_Node (Full)); + -- Propagate information of type invariants, which may be specified + -- for the full view. + + if Has_Invariants (Full) and not Has_Invariants (Priv) then + Set_Has_Invariants (Priv); + Set_Subprograms_For_Type (Priv, Subprograms_For_Type (Full)); + end if; + if Is_Tagged_Type (Priv) and then Is_Tagged_Type (Full) and then not Error_Posted (Full) Index: einfo.adb =================================================================== --- einfo.adb (revision 192066) +++ einfo.adb (working copy) @@ -7113,6 +7113,7 @@ S := Subprograms_For_Type (Id); Set_Subprograms_For_Type (Id, V); + Set_Subprograms_For_Type (V, S); while Present (S) loop if Has_Invariants (S) then @@ -7121,8 +7122,6 @@ S := Subprograms_For_Type (S); end if; end loop; - - Set_Subprograms_For_Type (Id, V); end Set_Invariant_Procedure; ---------------------------- @@ -7137,6 +7136,7 @@ S := Subprograms_For_Type (Id); Set_Subprograms_For_Type (Id, V); + Set_Subprograms_For_Type (V, S); while Present (S) loop if Has_Predicates (S) then @@ -7145,8 +7145,6 @@ S := Subprograms_For_Type (S); end if; end loop; - - Set_Subprograms_For_Type (Id, V); end Set_Predicate_Function; ----------------- Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 192124) +++ sem_prag.adb (working copy) @@ -10329,6 +10329,7 @@ when Pragma_Invariant => Invariant : declare Type_Id : Node_Id; Typ : Entity_Id; + PDecl : Node_Id; Discard : Boolean; pragma Unreferenced (Discard); @@ -10380,8 +10381,13 @@ -- Note that the type has at least one invariant, and also that -- it has inheritable invariants if we have Invariant'Class. + -- Build the corresponding invariant procedure declaration, so + -- that calls to it can be generated before the body is built + -- (for example wihin an expression function). - Set_Has_Invariants (Typ); + PDecl := Build_Invariant_Procedure_Declaration (Typ); + Insert_After (N, PDecl); + Analyze (PDecl); if Class_Present (N) then Set_Has_Inheritable_Invariants (Typ); Index: sem_ch13.adb =================================================================== --- sem_ch13.adb (revision 192066) +++ sem_ch13.adb (working copy) @@ -4902,6 +4902,48 @@ end if; end Analyze_Record_Representation_Clause; + ------------------------------------------- + -- Build_Invariant_Procedure_Declaration -- + ------------------------------------------- + + function Build_Invariant_Procedure_Declaration + (Typ : Entity_Id) return Node_Id + is + Loc : constant Source_Ptr := Sloc (Typ); + Object_Entity : constant Entity_Id := + Make_Defining_Identifier (Loc, New_Internal_Name ('I')); + Spec : Node_Id; + SId : Entity_Id; + + begin + Set_Etype (Object_Entity, Typ); + + -- Check for duplicate definiations. + + if Has_Invariants (Typ) + and then Present (Invariant_Procedure (Typ)) + then + return Empty; + end if; + + SId := Make_Defining_Identifier (Loc, + Chars => New_External_Name (Chars (Typ), "Invariant")); + Set_Has_Invariants (SId); + Set_Has_Invariants (Typ); + Set_Ekind (SId, E_Procedure); + Set_Invariant_Procedure (Typ, SId); + + Spec := + Make_Procedure_Specification (Loc, + Defining_Unit_Name => SId, + Parameter_Specifications => New_List ( + Make_Parameter_Specification (Loc, + Defining_Identifier => Object_Entity, + Parameter_Type => New_Occurrence_Of (Typ, Loc)))); + + return Make_Subprogram_Declaration (Loc, Specification => Spec); + end Build_Invariant_Procedure_Declaration; + ------------------------------- -- Build_Invariant_Procedure -- ------------------------------- @@ -4936,12 +4978,11 @@ -- "inherited" to the exception message and generating an informational -- message about the inheritance of an invariant. - Object_Name : constant Name_Id := New_Internal_Name ('I'); + Object_Name : Name_Id; -- Name for argument of invariant procedure - Object_Entity : constant Node_Id := - Make_Defining_Identifier (Loc, Object_Name); - -- The procedure declaration entity for the argument + Object_Entity : Node_Id; + -- The entity of the formal for the procedure -------------------- -- Add_Invariants -- @@ -5140,8 +5181,30 @@ Stmts := No_List; PDecl := Empty; PBody := Empty; - Set_Etype (Object_Entity, Typ); + SId := Empty; + -- If the aspect specification exists for some view of the type, the + -- declaration for the procedure has been created. + + if Has_Invariants (Typ) then + SId := Invariant_Procedure (Typ); + end if; + + if Present (SId) then + PDecl := Unit_Declaration_Node (SId); + + else + PDecl := Build_Invariant_Procedure_Declaration (Typ); + end if; + + -- Recover formal of procedure, for use in the calls to invariant + -- functions (including inherited ones). + + Object_Entity := + Defining_Identifier + (First (Parameter_Specifications (Specification (PDecl)))); + Object_Name := Chars (Object_Entity); + -- Add invariants for the current type Add_Invariants (Typ, Inherit => False); @@ -5174,39 +5237,8 @@ if Stmts /= No_List then - -- Build procedure declaration + Spec := Copy_Separate_Tree (Specification (PDecl)); - SId := - Make_Defining_Identifier (Loc, - Chars => New_External_Name (Chars (Typ), "Invariant")); - Set_Has_Invariants (SId); - Set_Invariant_Procedure (Typ, SId); - - Spec := - Make_Procedure_Specification (Loc, - Defining_Unit_Name => SId, - Parameter_Specifications => New_List ( - Make_Parameter_Specification (Loc, - Defining_Identifier => Object_Entity, - Parameter_Type => New_Occurrence_Of (Typ, Loc)))); - - PDecl := Make_Subprogram_Declaration (Loc, Specification => Spec); - - -- Build procedure body - - SId := - Make_Defining_Identifier (Loc, - Chars => New_External_Name (Chars (Typ), "Invariant")); - - Spec := - Make_Procedure_Specification (Loc, - Defining_Unit_Name => SId, - Parameter_Specifications => New_List ( - Make_Parameter_Specification (Loc, - Defining_Identifier => - Make_Defining_Identifier (Loc, Object_Name), - Parameter_Type => New_Occurrence_Of (Typ, Loc)))); - PBody := Make_Subprogram_Body (Loc, Specification => Spec, @@ -5216,14 +5248,18 @@ Statements => Stmts)); -- Insert procedure declaration and spec at the appropriate points. + -- If declaration is already analyzed, it was processed by the + -- generated pragma. if Present (Private_Decls) then -- The spec goes at the end of visible declarations, but they have -- already been analyzed, so we need to explicitly do the analyze. - Append_To (Visible_Decls, PDecl); - Analyze (PDecl); + if not Analyzed (PDecl) then + Append_To (Visible_Decls, PDecl); + Analyze (PDecl); + end if; -- The body goes at the end of the private declarations, which we -- have not analyzed yet, so we do not need to perform an explicit @@ -5523,6 +5559,7 @@ Make_Defining_Identifier (Loc, Chars => New_External_Name (Chars (Typ), "Predicate")); Set_Has_Predicates (SId); + Set_Ekind (SId, E_Function); Set_Predicate_Function (Typ, SId); -- The predicate function is shared between views of a type. Index: sem_ch13.ads =================================================================== --- sem_ch13.ads (revision 192066) +++ sem_ch13.ads (working copy) @@ -46,6 +46,14 @@ -- order is specified and there is at least one component clause. Adjusts -- component positions according to either Ada 95 or Ada 2005 (AI-133). + function Build_Invariant_Procedure_Declaration + (Typ : Entity_Id) return Node_Id; + -- If a type declaration has a specified invariant aspect, build the + -- declaration for the procedure at once, so that calls to it can be + -- generated before the body of the invariant procedure is built. This + -- is needed in the presence of public expression functions that return + -- the type in question. + procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id); -- Typ is a private type with invariants (indicated by Has_Invariants being -- set for Typ, indicating the presence of pragma Invariant entries on the