===================================================================
@@ -4475,6 +4475,8 @@
procedure Analyze_Private_Extension_Declaration (N : Node_Id) is
Indic : constant Node_Id := Subtype_Indication (N);
T : constant Entity_Id := Defining_Identifier (N);
+ Iface : Entity_Id;
+ Iface_Elmt : Elmt_Id;
Parent_Base : Entity_Id;
Parent_Type : Entity_Id;
@@ -4540,8 +4542,8 @@
elsif Is_Concurrent_Type (Parent_Type) then
Error_Msg_N
- ("parent type of a private extension cannot be "
- & "a synchronized tagged type (RM 3.9.1 (3/1))", N);
+ ("parent type of a private extension cannot be a synchronized "
+ & "tagged type (RM 3.9.1 (3/1))", N);
Set_Etype (T, Any_Type);
Set_Ekind (T, E_Limited_Private_Type);
@@ -4562,7 +4564,6 @@
if (not Is_Package_Or_Generic_Package (Current_Scope)
and then Nkind (Parent (N)) /= N_Generic_Subprogram_Declaration)
or else In_Private_Part (Current_Scope)
-
then
Error_Msg_N ("invalid context for private extension", N);
end if;
@@ -4589,13 +4590,26 @@
Build_Derived_Record_Type (N, Parent_Type, T);
- -- Propagate inherited invariant information. The new type has
- -- invariants, if the parent type has inheritable invariants,
- -- and these invariants can in turn be inherited.
+ -- A private extension inherits any class-wide invariants coming from a
+ -- parent type or an interface. Note that the invariant procedure of the
+ -- parent type should not be inherited because the private extension may
+ -- define invariants of its own.
if Has_Inheritable_Invariants (Parent_Type) then
- Set_Has_Inheritable_Invariants (T);
- Set_Has_Invariants (T);
+ Set_Has_Inherited_Invariants (T);
+
+ elsif Present (Interfaces (T)) then
+ Iface_Elmt := First_Elmt (Interfaces (T));
+ while Present (Iface_Elmt) loop
+ Iface := Node (Iface_Elmt);
+
+ if Has_Inheritable_Invariants (Iface) then
+ Set_Has_Inherited_Invariants (T);
+ exit;
+ end if;
+
+ Next_Elmt (Iface_Elmt);
+ end loop;
end if;
-- Ada 2005 (AI-443): Synchronized private extension or a rewritten
@@ -4617,33 +4631,29 @@
(not Is_Interface (Parent_Type)
or else not Is_Synchronized_Interface (Parent_Type))
then
- Error_Msg_NE ("parent type of & must be tagged limited " &
- "or synchronized", N, T);
+ Error_Msg_NE
+ ("parent type of & must be tagged limited or synchronized",
+ N, T);
end if;
-- The progenitors (if any) must be limited or synchronized
-- interfaces.
if Present (Interfaces (T)) then
- declare
- Iface : Entity_Id;
- Iface_Elmt : Elmt_Id;
+ Iface_Elmt := First_Elmt (Interfaces (T));
+ while Present (Iface_Elmt) loop
+ Iface := Node (Iface_Elmt);
- begin
- Iface_Elmt := First_Elmt (Interfaces (T));
- while Present (Iface_Elmt) loop
- Iface := Node (Iface_Elmt);
+ if not Is_Limited_Interface (Iface)
+ and then not Is_Synchronized_Interface (Iface)
+ then
+ Error_Msg_NE
+ ("progenitor & must be limited or synchronized",
+ N, Iface);
+ end if;
- if not Is_Limited_Interface (Iface)
- and then not Is_Synchronized_Interface (Iface)
- then
- Error_Msg_NE ("progenitor & must be limited " &
- "or synchronized", N, Iface);
- end if;
-
- Next_Elmt (Iface_Elmt);
- end loop;
- end;
+ Next_Elmt (Iface_Elmt);
+ end loop;
end if;
-- Regular derived extension, the parent must be a limited or
@@ -5154,10 +5164,9 @@
if Has_Predicates (T)
and then Present (Predicate_Function (T))
-
- and then
- ((In_Instance and then not Comes_From_Source (N))
- or else No (Aspect_Specifications (N)))
+ and then
+ ((In_Instance and then not Comes_From_Source (N))
+ or else No (Aspect_Specifications (N)))
then
Set_Subprograms_For_Type (Id, Subprograms_For_Type (T));
@@ -5167,6 +5176,11 @@
end if;
end if;
+ -- Propagate invariant-related attributes from the base type to the
+ -- subtype.
+
+ Propagate_Invariant_Attributes (Id, From_Typ => Base_Type (T));
+
-- Remaining processing depends on characteristics of base type
T := Etype (Id);
@@ -5228,9 +5242,9 @@
if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then
if Is_Scalar_Type (Etype (Id))
- and then Scalar_Range (Id) /=
- Scalar_Range (Etype (Subtype_Mark
- (Subtype_Indication (N))))
+ and then Scalar_Range (Id) /=
+ Scalar_Range
+ (Etype (Subtype_Mark (Subtype_Indication (N))))
then
Apply_Range_Check
(Scalar_Range (Id),
@@ -5301,14 +5315,6 @@
end if;
end if;
- -- A type invariant applies to any subtype in its scope, in particular
- -- to a generic actual.
-
- if Has_Invariants (T) and then In_Open_Scopes (Scope (T)) then
- Set_Has_Invariants (Id);
- Set_Invariant_Procedure (Id, Invariant_Procedure (T));
- end if;
-
Set_Optimize_Alignment_Flags (Id);
Check_Eliminated (Id);
@@ -5633,16 +5639,20 @@
-- Complete setup of implicit base type
- Set_First_Index (Implicit_Base, First_Index (T));
- Set_Component_Type (Implicit_Base, Element_Type);
+ Set_Component_Size (Implicit_Base, Uint_0);
+ Set_Component_Type (Implicit_Base, Element_Type);
+ Set_Finalize_Storage_Only
+ (Implicit_Base,
+ Finalize_Storage_Only (Element_Type));
+ Set_First_Index (Implicit_Base, First_Index (T));
+ Set_Has_Controlled_Component
+ (Implicit_Base,
+ Has_Controlled_Component (Element_Type)
+ or else Is_Controlled_Active (Element_Type));
+ Set_Packed_Array_Impl_Type
+ (Implicit_Base, Empty);
+
Propagate_Concurrent_Flags (Implicit_Base, Element_Type);
- Set_Component_Size (Implicit_Base, Uint_0);
- Set_Packed_Array_Impl_Type (Implicit_Base, Empty);
- Set_Has_Controlled_Component (Implicit_Base,
- Has_Controlled_Component (Element_Type)
- or else Is_Controlled_Active (Element_Type));
- Set_Finalize_Storage_Only (Implicit_Base,
- Finalize_Storage_Only (Element_Type));
-- Inherit the "ghostness" from the constrained array type
@@ -8786,31 +8796,35 @@
end;
end if;
- -- Propagate inherited invariant information of parents
- -- and progenitors
+ -- A derived type inherits any class-wide invariants coming
+ -- from a parent type or an interface. Note that the invariant
+ -- procedure of the parent type should not be inherited because
+ -- the derived type may define invariants of its own.
if Ada_Version >= Ada_2012
and then not Is_Interface (Derived_Type)
then
- if Has_Inheritable_Invariants (Parent_Type) then
- Set_Has_Invariants (Derived_Type);
- Set_Has_Inheritable_Invariants (Derived_Type);
+ if Has_Inherited_Invariants (Parent_Type)
+ or else Has_Inheritable_Invariants (Parent_Type)
+ then
+ Set_Has_Inherited_Invariants (Derived_Type);
elsif not Is_Empty_Elmt_List (Ifaces_List) then
declare
- AI : Elmt_Id;
+ Iface : Entity_Id;
+ Iface_Elmt : Elmt_Id;
begin
- AI := First_Elmt (Ifaces_List);
- while Present (AI) loop
- if Has_Inheritable_Invariants (Node (AI)) then
- Set_Has_Invariants (Derived_Type);
- Set_Has_Inheritable_Invariants (Derived_Type);
+ Iface_Elmt := First_Elmt (Ifaces_List);
+ while Present (Iface_Elmt) loop
+ Iface := Node (Iface_Elmt);
+ if Has_Inheritable_Invariants (Iface) then
+ Set_Has_Inherited_Invariants (Derived_Type);
exit;
end if;
- Next_Elmt (AI);
+ Next_Elmt (Iface_Elmt);
end loop;
end;
end if;
@@ -16427,63 +16441,93 @@
function Find_Type_Name (N : Node_Id) return Entity_Id is
Id : constant Entity_Id := Defining_Identifier (N);
+ New_Id : Entity_Id;
Prev : Entity_Id;
- New_Id : Entity_Id;
Prev_Par : Node_Id;
procedure Check_Duplicate_Aspects;
-- Check that aspects specified in a completion have not been specified
- -- already in the partial view. Type_Invariant and others can be
- -- specified on either view but never on both.
+ -- already in the partial view.
procedure Tag_Mismatch;
- -- Diagnose a tagged partial view whose full view is untagged.
- -- We post the message on the full view, with a reference to
- -- the previous partial view. The partial view can be private
- -- or incomplete, and these are handled in a different manner,
- -- so we determine the position of the error message from the
- -- respective slocs of both.
+ -- Diagnose a tagged partial view whose full view is untagged. We post
+ -- the message on the full view, with a reference to the previous
+ -- partial view. The partial view can be private or incomplete, and
+ -- these are handled in a different manner, so we determine the position
+ -- of the error message from the respective slocs of both.
-----------------------------
-- Check_Duplicate_Aspects --
-----------------------------
procedure Check_Duplicate_Aspects is
- Prev_Aspects : constant List_Id := Aspect_Specifications (Prev_Par);
- Full_Aspects : constant List_Id := Aspect_Specifications (N);
- F_Spec, P_Spec : Node_Id;
+ function Get_Partial_View_Aspect (Asp : Node_Id) return Node_Id;
+ -- Return the corresponding aspect of the partial view which matches
+ -- the aspect id of Asp. Return Empty is no such aspect exists.
+ -----------------------------
+ -- Get_Partial_View_Aspect --
+ -----------------------------
+
+ function Get_Partial_View_Aspect (Asp : Node_Id) return Node_Id is
+ Asp_Id : constant Aspect_Id := Get_Aspect_Id (Asp);
+ Prev_Asps : constant List_Id := Aspect_Specifications (Prev_Par);
+ Prev_Asp : Node_Id;
+
+ begin
+ if Present (Prev_Asps) then
+ Prev_Asp := First (Prev_Asps);
+ while Present (Prev_Asp) loop
+ if Get_Aspect_Id (Prev_Asp) = Asp_Id then
+ return Prev_Asp;
+ end if;
+
+ Next (Prev_Asp);
+ end loop;
+ end if;
+
+ return Empty;
+ end Get_Partial_View_Aspect;
+
+ -- Local variables
+
+ Full_Asps : constant List_Id := Aspect_Specifications (N);
+ Full_Asp : Node_Id;
+ Part_Asp : Node_Id;
+
+ -- Start of processing for Check_Duplicate_Aspects
+
begin
- if Present (Full_Aspects) then
- F_Spec := First (Full_Aspects);
- while Present (F_Spec) loop
- if Present (Prev_Aspects) then
- P_Spec := First (Prev_Aspects);
- while Present (P_Spec) loop
- if Chars (Identifier (P_Spec)) =
- Chars (Identifier (F_Spec))
- then
- Error_Msg_N
- ("aspect already specified in private declaration",
- F_Spec);
- Remove (F_Spec);
- return;
- end if;
+ if Present (Full_Asps) then
+ Full_Asp := First (Full_Asps);
+ while Present (Full_Asp) loop
+ Part_Asp := Get_Partial_View_Aspect (Full_Asp);
- Next (P_Spec);
- end loop;
+ -- An aspect and its class-wide counterpart are two distinct
+ -- aspects and may apply to both views of an entity.
+
+ if Present (Part_Asp)
+ and then Class_Present (Part_Asp) = Class_Present (Full_Asp)
+ then
+ Error_Msg_N
+ ("aspect already specified in private declaration",
+ Full_Asp);
+
+ Remove (Full_Asp);
+ return;
end if;
if Has_Discriminants (Prev)
and then not Has_Unknown_Discriminants (Prev)
- and then Chars (Identifier (F_Spec)) =
- Name_Implicit_Dereference
+ and then Get_Aspect_Id (Full_Asp) =
+ Aspect_Implicit_Dereference
then
- Error_Msg_N ("cannot specify aspect " &
- "if partial view has known discriminants", F_Spec);
+ Error_Msg_N
+ ("cannot specify aspect if partial view has known "
+ & "discriminants", Full_Asp);
end if;
- Next (F_Spec);
+ Next (Full_Asp);
end loop;
end if;
end Check_Duplicate_Aspects;
@@ -19573,8 +19617,8 @@
and then not Is_Ancestor (Base_Type (Priv_Parent), Full_Parent)
then
Error_Msg_N
- ("parent of full type must descend from parent"
- & " of private extension", Full_Indic);
+ ("parent of full type must descend from parent of private "
+ & "extension", Full_Indic);
-- First check a formal restriction, and then proceed with checking
-- Ada rules. Since the formal restriction is not a serious error, we
@@ -19628,9 +19672,9 @@
while Present (Priv_Discr) and then Present (Full_Discr) loop
if Original_Record_Component (Priv_Discr) =
Original_Record_Component (Full_Discr)
- or else
- Corresponding_Discriminant (Priv_Discr) =
- Corresponding_Discriminant (Full_Discr)
+ or else
+ Corresponding_Discriminant (Priv_Discr) =
+ Corresponding_Discriminant (Full_Discr)
then
null;
else
@@ -19643,8 +19687,8 @@
if Present (Priv_Discr) or else Present (Full_Discr) then
Error_Msg_N
- ("full view must inherit discriminants of the parent"
- & " type used in the private extension", Full_Indic);
+ ("full view must inherit discriminants of the parent "
+ & "type used in the private extension", Full_Indic);
elsif Priv_Constr and then not Full_Constr then
Error_Msg_N
@@ -19662,13 +19706,13 @@
-- known or unknown discriminants, then the full type
-- declaration shall define a definite subtype.
- elsif not Has_Unknown_Discriminants (Priv_T)
+ elsif not Has_Unknown_Discriminants (Priv_T)
and then not Has_Discriminants (Priv_T)
and then not Is_Constrained (Full_T)
then
Error_Msg_N
- ("full view must define a constrained type if partial view"
- & " has no discriminants", Full_T);
+ ("full view must define a constrained type if partial view "
+ & "has no discriminants", Full_T);
end if;
-- ??????? Do we implement the following properly ?????
@@ -20095,42 +20139,33 @@
Mark_Full_View_As_Ghost (Priv_T, Full_T);
end if;
- -- Propagate invariants to full type
+ -- Propagate invariant-related attributes from the private view to the
+ -- full view and its base type.
- if Has_Invariants (Priv_T) then
- Set_Has_Invariants (Full_T);
- Set_Invariant_Procedure (Full_T, Invariant_Procedure (Priv_T));
- end if;
+ Propagate_Invariant_Attributes (Full_T, From_Typ => Priv_T);
+ Propagate_Invariant_Attributes (Base_Type (Full_T), From_Typ => Priv_T);
- if Has_Inheritable_Invariants (Priv_T) then
- Set_Has_Inheritable_Invariants (Full_T);
- end if;
+ -- AI12-0041: Detect an attempt to inherit a class-wide type invariant
+ -- in the full view without advertising the inheritance in the partial
+ -- view. This can only occur when the partial view has no parent type
+ -- and the full view has an interface as a parent. Any other scenarios
+ -- are illegal because implemented interfaces must match between the
+ -- two views.
- -- Check hidden inheritance of class-wide type invariants
-
- if Ada_Version >= Ada_2012
- and then not Has_Inheritable_Invariants (Full_T)
- and then In_Private_Part (Current_Scope)
- and then Has_Interfaces (Full_T)
- then
+ if Is_Tagged_Type (Priv_T) and then Is_Tagged_Type (Full_T) then
declare
- Ifaces : Elist_Id;
- AI : Elmt_Id;
+ Full_Par : constant Entity_Id := Etype (Full_T);
+ Priv_Par : constant Entity_Id := Etype (Priv_T);
begin
- Collect_Interfaces (Full_T, Ifaces, Exclude_Parents => True);
-
- AI := First_Elmt (Ifaces);
- while Present (AI) loop
- if Has_Inheritable_Invariants (Node (AI)) then
- Error_Msg_N
- ("hidden inheritance of class-wide type invariants " &
- "not allowed", N);
- exit;
- end if;
-
- Next_Elmt (AI);
- end loop;
+ if not Is_Interface (Priv_Par)
+ and then Is_Interface (Full_Par)
+ and then Has_Inheritable_Invariants (Full_Par)
+ then
+ Error_Msg_N
+ ("hidden inheritance of class-wide type invariants not "
+ & "allowed", N);
+ end if;
end;
end if;
@@ -20952,34 +20987,31 @@
Private_To_Full_View : Boolean := False)
is
procedure Remove_Default_Init_Cond_Procedure (Typ : Entity_Id);
- -- Remove the default initial procedure (if any) from the rep chain of
- -- type Typ.
+ -- Remove the default initial condition procedure (if any) from the
+ -- Subprograms_For_Type chain of type Typ.
----------------------------------------
-- Remove_Default_Init_Cond_Procedure --
----------------------------------------
procedure Remove_Default_Init_Cond_Procedure (Typ : Entity_Id) is
- Found : Boolean := False;
- Prev : Entity_Id;
- Subp : Entity_Id;
+ Subps : constant Elist_Id := Subprograms_For_Type (Typ);
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
begin
- Prev := Typ;
- Subp := Subprograms_For_Type (Typ);
- while Present (Subp) loop
- if Is_Default_Init_Cond_Procedure (Subp) then
- Found := True;
- exit;
- end if;
+ if Present (Subps) then
+ Subp_Elmt := First_Elmt (Subps);
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
- Prev := Subp;
- Subp := Subprograms_For_Type (Subp);
- end loop;
+ if Is_Default_Init_Cond_Procedure (Subp_Id) then
+ Remove_Elmt (Subps, Subp_Elmt);
+ exit;
+ end if;
- if Found then
- Set_Subprograms_For_Type (Prev, Subprograms_For_Type (Subp));
- Set_Subprograms_For_Type (Subp, Empty);
+ Next_Elmt (Subp_Elmt);
+ end loop;
end if;
end Remove_Default_Init_Cond_Procedure;
===================================================================
@@ -55,12 +55,15 @@
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Ch3; use Sem_Ch3;
+with Sem_Ch6; use Sem_Ch6;
with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch13; use Sem_Ch13;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Snames; use Snames;
with Stand; use Stand;
+with Stringt; use Stringt;
with Tbuild; use Tbuild;
with Ttypes; use Ttypes;
with Uintp; use Uintp;
@@ -3438,6 +3441,1518 @@
Expand_At_End_Handler (HSS, Empty);
end Build_Finalizer_Call;
+ ------------------------------------
+ -- Build_Invariant_Procedure_Body --
+ ------------------------------------
+
+ procedure Build_Invariant_Procedure_Body
+ (Typ : Entity_Id;
+ Partial_Invariant : Boolean := False)
+ is
+ Loc : constant Source_Ptr := Sloc (Typ);
+
+ Pragmas_Seen : Elist_Id := No_Elist;
+ -- This list contains all invariant pragmas processed so far. The list
+ -- is used to avoid generating redundant invariant checks.
+
+ Produced_Check : Boolean := False;
+ -- This flag tracks whether the type has produced at least one invariant
+ -- check. The flag is used as a sanity check at the end of the routine.
+
+ -- NOTE: most of the routines in Build_Invariant_Procedure_Body are
+ -- intentionally unnested to avoid deep indentation of code.
+
+ -- NOTE: all Add_xxx_Invariants routines are reactive. In other words
+ -- they emit checks, loops (for arrays) and case statements (for record
+ -- variant parts) only when there are invariants to verify. This keeps
+ -- the body of the invariant procedure free from useless code.
+
+ procedure Add_Array_Component_Invariants
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id);
+ -- Generate an invariant check for each component of array type T.
+ -- Obj_Id denotes the entity of the _object formal parameter of the
+ -- invariant procedure. All created checks are added to list Checks.
+
+ procedure Add_Interface_Invariants
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id);
+ -- Generate an invariant check for each inherited class-wide invariant
+ -- coming from all interfaces implemented by type T. Obj_Id denotes the
+ -- entity of the _object formal parameter of the invariant procedure.
+ -- All created checks are added to list Checks.
+
+ procedure Add_Parent_Invariants
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id);
+ -- Generate an invariant check for each inherited class-wide invariant
+ -- coming from all parent types of type T. Obj_Id denotes the entity of
+ -- the _object formal parameter of the invariant procedure. All created
+ -- checks are added to list Checks.
+
+ procedure Add_Record_Component_Invariants
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id);
+ -- Generate an invariant check for each component of record type T.
+ -- Obj_Id denotes the entity of the _object formal parameter of the
+ -- invariant procedure. All created checks are added to list Checks.
+
+ procedure Add_Type_Invariants
+ (Priv_Typ : Entity_Id;
+ Full_Typ : Entity_Id;
+ CRec_Typ : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id;
+ Inherit : Boolean := False;
+ Priv_Item : Node_Id := Empty);
+ -- Generate an invariant check for each invariant found in one of the
+ -- following types (if available):
+ --
+ -- Priv_Typ - the partial view of a type
+ -- Full_Typ - the full view of a type
+ -- CRec_Typ - the corresponding record of a protected or a task type
+ --
+ -- Obj_Id denotes the entity of the _object formal parameter of the
+ -- invariant procedure. All created checks are added to list Checks.
+ -- Flag Inherit should be set when generating invariant checks for
+ -- inherited class-wide invariants. Priv_Item denotes the first rep
+ -- item of the private type.
+
+ procedure Create_Append (L : in out List_Id; N : Node_Id);
+ -- Append arbitrary node N to list L. If there is no list, create one.
+
+ function Is_Untagged_Private_Derivation
+ (Priv_Typ : Entity_Id;
+ Full_Typ : Entity_Id) return Boolean;
+ -- Determine whether private type Priv_Typ and its full view Full_Typ
+ -- represent an untagged derivation from a private parent.
+
+ ------------------------------------
+ -- Add_Array_Component_Invariants --
+ ------------------------------------
+
+ procedure Add_Array_Component_Invariants
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id)
+ is
+ Comp_Typ : constant Entity_Id := Component_Type (T);
+ Dims : constant Pos := Number_Dimensions (T);
+
+ procedure Process_Array_Component
+ (Indices : List_Id;
+ Comp_Checks : in out List_Id);
+ -- Generate an invariant check for an array component identified by
+ -- the indices in list Indices. All created checks are added to list
+ -- Comp_Checks.
+
+ procedure Process_One_Dimension
+ (Dim : Pos;
+ Indices : List_Id;
+ Dim_Checks : in out List_Id);
+ -- Generate a loop over the Nth dimension Dim of an array type. List
+ -- Indices contains all array indices for the dimension. All created
+ -- checks are added to list Dim_Checks.
+
+ -----------------------------
+ -- Process_Array_Component --
+ -----------------------------
+
+ procedure Process_Array_Component
+ (Indices : List_Id;
+ Comp_Checks : in out List_Id)
+ is
+ Proc_Id : Entity_Id;
+
+ begin
+ if Has_Invariants (Comp_Typ) then
+ Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
+
+ -- The component type should have an invariant procedure if it
+ -- has invariants of its own or inherits class-wide invariants
+ -- from parent or interface types.
+
+ pragma Assert (Present (Proc_Id));
+
+ -- Generate:
+ -- <Comp_Typ>Invariant (_object (<Indices>));
+
+ -- Note that the invariant procedure may have a null body if
+ -- assertions are disabled or Assertion_Polity Ignore is in
+ -- effect.
+
+ if not Has_Null_Body (Proc_Id) then
+ Create_Append (Comp_Checks,
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of (Proc_Id, Loc),
+ Parameter_Associations => New_List (
+ Make_Indexed_Component (Loc,
+ Prefix => New_Occurrence_Of (Obj_Id, Loc),
+ Expressions => New_Copy_List (Indices)))));
+ end if;
+
+ Produced_Check := True;
+ end if;
+
+ -- In a rare case the designated type of an access component may
+ -- have an invariant. In this case verify the dereference of the
+ -- component.
+
+ if Is_Access_Type (Comp_Typ)
+ and then Has_Invariants (Designated_Type (Comp_Typ))
+ then
+ Proc_Id :=
+ Invariant_Procedure (Base_Type (Designated_Type (Comp_Typ)));
+
+ -- The designated type should have an invariant procedure if it
+ -- has invariants of its own or inherits class-wide invariants
+ -- from parent or interface types.
+
+ pragma Assert (Present (Proc_Id));
+
+ -- Generate:
+ -- if _object (<Indexes>) /= null then
+ -- <Desig_Comp_Typ>Invariant (_object (<Indices>).all);
+ -- end if;
+
+ -- Note that the invariant procedure may have a null body if
+ -- assertions are disabled or Assertion_Polity Ignore is in
+ -- effect.
+
+ if not Has_Null_Body (Proc_Id) then
+ Create_Append (Comp_Checks,
+ Make_If_Statement (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd =>
+ Make_Indexed_Component (Loc,
+ Prefix => New_Occurrence_Of (Obj_Id, Loc),
+ Expressions => New_Copy_List (Indices)),
+ Right_Opnd => Make_Null (Loc)),
+
+ Then_Statements => New_List (
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of (Proc_Id, Loc),
+
+ Parameter_Associations => New_List (
+ Make_Explicit_Dereference (Loc,
+ Prefix =>
+ Make_Indexed_Component (Loc,
+ Prefix =>
+ New_Occurrence_Of (Obj_Id, Loc),
+ Expressions =>
+ New_Copy_List (Indices))))))));
+ end if;
+
+ Produced_Check := True;
+ end if;
+ end Process_Array_Component;
+
+ ---------------------------
+ -- Process_One_Dimension --
+ ---------------------------
+
+ procedure Process_One_Dimension
+ (Dim : Pos;
+ Indices : List_Id;
+ Dim_Checks : in out List_Id)
+ is
+ Comp_Checks : List_Id := No_List;
+ Index : Entity_Id;
+
+ begin
+ -- Generate the invariant checks for the array component after all
+ -- dimensions have produced their respective loops.
+
+ if Dim > Dims then
+ Process_Array_Component
+ (Indices => Indices,
+ Comp_Checks => Dim_Checks);
+
+ -- Otherwise create a loop for the current dimension
+
+ else
+ -- Create a new loop variable for each dimension
+
+ Index :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name ('I', Dim));
+ Append_To (Indices, New_Occurrence_Of (Index, Loc));
+
+ Process_One_Dimension
+ (Dim => Dim + 1,
+ Indices => Indices,
+ Dim_Checks => Comp_Checks);
+
+ -- Generate:
+ -- for I<Dim> in _object'Range (<Dim>) loop
+ -- <Comp_Checks>
+ -- end loop;
+
+ -- Note that the invariant procedure may have a null body if
+ -- assertions are disabled or Assertion_Polity Ignore is in
+ -- effect.
+
+ if Present (Comp_Checks) then
+ Create_Append (Dim_Checks,
+ Make_Implicit_Loop_Statement (T,
+ Identifier => Empty,
+ Iteration_Scheme =>
+ Make_Iteration_Scheme (Loc,
+ Loop_Parameter_Specification =>
+ Make_Loop_Parameter_Specification (Loc,
+ Defining_Identifier => Index,
+ Discrete_Subtype_Definition =>
+ Make_Attribute_Reference (Loc,
+ Prefix =>
+ New_Occurrence_Of (Obj_Id, Loc),
+ Attribute_Name => Name_Range,
+ Expressions => New_List (
+ Make_Integer_Literal (Loc, Dim))))),
+
+ Statements => Comp_Checks));
+ end if;
+ end if;
+ end Process_One_Dimension;
+
+ -- Start of processing for Add_Array_Component_Invariants
+
+ begin
+ Process_One_Dimension
+ (Dim => 1,
+ Indices => New_List,
+ Dim_Checks => Checks);
+ end Add_Array_Component_Invariants;
+
+ ------------------------------
+ -- Add_Interface_Invariants --
+ ------------------------------
+
+ procedure Add_Interface_Invariants
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id)
+ is
+ Iface_Elmt : Elmt_Id;
+ Ifaces : Elist_Id;
+
+ begin
+ if Is_Tagged_Type (T) then
+ Collect_Interfaces (T, Ifaces);
+
+ -- Process the class-wide invariants of all implemented interfaces
+
+ Iface_Elmt := First_Elmt (Ifaces);
+ while Present (Iface_Elmt) loop
+ Add_Type_Invariants
+ (Priv_Typ => Empty,
+ Full_Typ => Node (Iface_Elmt),
+ CRec_Typ => Empty,
+ Obj_Id => Obj_Id,
+ Checks => Checks,
+ Inherit => True);
+
+ Next_Elmt (Iface_Elmt);
+ end loop;
+ end if;
+ end Add_Interface_Invariants;
+
+ ---------------------------
+ -- Add_Parent_Invariants --
+ ---------------------------
+
+ procedure Add_Parent_Invariants
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id)
+ is
+ Dummy_1 : Entity_Id;
+ Dummy_2 : Entity_Id;
+
+ Curr_Typ : Entity_Id;
+ -- The entity of the current type being examined
+
+ Full_Typ : Entity_Id;
+ -- The full view of Par_Typ
+
+ Par_Typ : Entity_Id;
+ -- The entity of the parent type
+
+ Priv_Typ : Entity_Id;
+ -- The partial view of Par_Typ
+
+ begin
+ -- Climb the parent type chain
+
+ Curr_Typ := T;
+ loop
+ -- Do not consider subtypes as they inherit the invariants from
+ -- their base types.
+
+ Par_Typ := Base_Type (Etype (Curr_Typ));
+
+ -- Stop the climb once the root of the parent chain is reached
+
+ exit when Curr_Typ = Par_Typ;
+
+ -- Process the class-wide invariants of the parent type
+
+ Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2);
+
+ Add_Type_Invariants
+ (Priv_Typ => Priv_Typ,
+ Full_Typ => Full_Typ,
+ CRec_Typ => Empty,
+ Obj_Id => Obj_Id,
+ Checks => Checks,
+ Inherit => True);
+
+ Curr_Typ := Par_Typ;
+ end loop;
+ end Add_Parent_Invariants;
+
+ -------------------------------------
+ -- Add_Record_Component_Invariants --
+ -------------------------------------
+
+ procedure Add_Record_Component_Invariants
+ (T : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id)
+ is
+ procedure Process_Component_List
+ (Comp_List : Node_Id;
+ CL_Checks : in out List_Id);
+ -- Generate invariant checks for all record components found in
+ -- component list Comp_List, including variant parts. All created
+ -- checks are added to list CL_Checks.
+
+ procedure Process_Record_Component
+ (Comp_Id : Entity_Id;
+ Comp_Checks : in out List_Id);
+ -- Generate an invariant check for a record component identified by
+ -- Comp_Id. All created checks are added to list Comp_Checks.
+
+ ----------------------------
+ -- Process_Component_List --
+ ----------------------------
+
+ procedure Process_Component_List
+ (Comp_List : Node_Id;
+ CL_Checks : in out List_Id)
+ is
+ Comp : Node_Id;
+ Var : Node_Id;
+ Var_Alts : List_Id := No_List;
+ Var_Checks : List_Id := No_List;
+ Var_Stmts : List_Id;
+
+ Produced_Variant_Check : Boolean := False;
+ -- This flag tracks whether the component has produced at least
+ -- one invariant check.
+
+ begin
+ -- Traverse the component items
+
+ Comp := First (Component_Items (Comp_List));
+ while Present (Comp) loop
+ if Nkind (Comp) = N_Component_Declaration then
+
+ -- Generate the component invariant check
+
+ Process_Record_Component
+ (Comp_Id => Defining_Entity (Comp),
+ Comp_Checks => CL_Checks);
+ end if;
+
+ Next (Comp);
+ end loop;
+
+ -- Traverse the variant part
+
+ if Present (Variant_Part (Comp_List)) then
+ Var := First (Variants (Variant_Part (Comp_List)));
+ while Present (Var) loop
+ Var_Checks := No_List;
+
+ -- Generate invariant checks for all components and variant
+ -- parts that qualify.
+
+ Process_Component_List
+ (Comp_List => Component_List (Var),
+ CL_Checks => Var_Checks);
+
+ -- The components of the current variant produced at least
+ -- one invariant check.
+
+ if Present (Var_Checks) then
+ Var_Stmts := Var_Checks;
+ Produced_Variant_Check := True;
+
+ -- Otherwise there are either no components with invariants,
+ -- assertions are disabled, or Assertion_Policy Ignore is in
+ -- effect.
+
+ else
+ Var_Stmts := New_List (Make_Null_Statement (Loc));
+ end if;
+
+ Create_Append (Var_Alts,
+ Make_Case_Statement_Alternative (Loc,
+ Discrete_Choices =>
+ New_Copy_List (Discrete_Choices (Var)),
+ Statements => Var_Stmts));
+
+ Next (Var);
+ end loop;
+
+ -- Create a case statement which verifies the invariant checks
+ -- of a particular component list depending on the discriminant
+ -- values only when there is at least one real invariant check.
+
+ if Produced_Variant_Check then
+ Create_Append (CL_Checks,
+ Make_Case_Statement (Loc,
+ Expression =>
+ Make_Selected_Component (Loc,
+ Prefix => New_Occurrence_Of (Obj_Id, Loc),
+ Selector_Name =>
+ New_Occurrence_Of
+ (Entity (Name (Variant_Part (Comp_List))), Loc)),
+ Alternatives => Var_Alts));
+ end if;
+ end if;
+ end Process_Component_List;
+
+ ------------------------------
+ -- Process_Record_Component --
+ ------------------------------
+
+ procedure Process_Record_Component
+ (Comp_Id : Entity_Id;
+ Comp_Checks : in out List_Id)
+ is
+ Comp_Typ : constant Entity_Id := Etype (Comp_Id);
+ Proc_Id : Entity_Id;
+
+ Produced_Component_Check : Boolean := False;
+ -- This flag tracks whether the component has produced at least
+ -- one invariant check.
+
+ begin
+ -- Nothing to do for internal component _parent. Note that it is
+ -- not desirable to check whether the component comes from source
+ -- because protected type components are relocated to an internal
+ -- corresponding record, but still need processing.
+
+ if Chars (Comp_Id) = Name_uParent then
+ return;
+ end if;
+
+ -- Verify the invariant of the component. Note that an access
+ -- type may have an invariant when it acts as the full view of a
+ -- private type and the invariant appears on the partial view. In
+ -- this case verify the access value itself.
+
+ if Has_Invariants (Comp_Typ) then
+ Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
+
+ -- The component type should have an invariant procedure if it
+ -- has invariants of its own or inherits class-wide invariants
+ -- from parent or interface types.
+
+ pragma Assert (Present (Proc_Id));
+
+ -- Generate:
+ -- <Comp_Typ>Invariant (T (_object).<Comp_Id>);
+
+ -- Note that the invariant procedure may have a null body if
+ -- assertions are disabled or Assertion_Polity Ignore is in
+ -- effect.
+
+ if not Has_Null_Body (Proc_Id) then
+ Create_Append (Comp_Checks,
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of (Proc_Id, Loc),
+ Parameter_Associations => New_List (
+ Make_Selected_Component (Loc,
+ Prefix =>
+ Unchecked_Convert_To
+ (T, New_Occurrence_Of (Obj_Id, Loc)),
+ Selector_Name =>
+ New_Occurrence_Of (Comp_Id, Loc)))));
+ end if;
+
+ Produced_Check := True;
+ Produced_Component_Check := True;
+ end if;
+
+ -- In a rare case the designated type of an access component may
+ -- have a invariant. In this case verify the dereference of the
+ -- component.
+
+ if Is_Access_Type (Comp_Typ)
+ and then Has_Invariants (Designated_Type (Comp_Typ))
+ then
+ Proc_Id :=
+ Invariant_Procedure (Base_Type (Designated_Type (Comp_Typ)));
+
+ -- The designated type should have an invariant procedure if it
+ -- has invariants of its own or inherits class-wide invariants
+ -- from parent or interface types.
+
+ pragma Assert (Present (Proc_Id));
+
+ -- Generate:
+ -- if T (_object).<Comp_Id> /= null then
+ -- <Desig_Comp_Typ>Invariant (T (_object).<Comp_Id>.all);
+ -- end if;
+
+ -- Note that the invariant procedure may have a null body if
+ -- assertions are disabled or Assertion_Polity Ignore is in
+ -- effect.
+
+ if not Has_Null_Body (Proc_Id) then
+ Create_Append (Comp_Checks,
+ Make_If_Statement (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd =>
+ Make_Selected_Component (Loc,
+ Prefix =>
+ Unchecked_Convert_To
+ (T, New_Occurrence_Of (Obj_Id, Loc)),
+ Selector_Name =>
+ New_Occurrence_Of (Comp_Id, Loc)),
+ Right_Opnd => Make_Null (Loc)),
+
+ Then_Statements => New_List (
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of (Proc_Id, Loc),
+
+ Parameter_Associations => New_List (
+ Make_Explicit_Dereference (Loc,
+ Prefix =>
+ Make_Selected_Component (Loc,
+ Prefix =>
+ Unchecked_Convert_To
+ (T, New_Occurrence_Of (Obj_Id, Loc)),
+ Selector_Name =>
+ New_Occurrence_Of (Comp_Id, Loc))))))));
+ end if;
+
+ Produced_Check := True;
+ Produced_Component_Check := True;
+ end if;
+
+ if Produced_Component_Check and then Has_Unchecked_Union (T) then
+ Error_Msg_NE
+ ("invariants cannot be checked on components of "
+ & "unchecked_union type &?", Comp_Id, T);
+ end if;
+ end Process_Record_Component;
+
+ -- Local variables
+
+ Comps : Node_Id;
+ Def : Node_Id;
+
+ -- Start of processing for Add_Record_Component_Invariants
+
+ begin
+ -- An untagged derived type inherits the components of its parent
+ -- type. In order to avoid creating redundant invariant checks, do
+ -- not process the components now. Instead wait until the ultimate
+ -- parent of the untagged derivation chain is reached.
+
+ if not Is_Untagged_Derivation (T) then
+ Def := Type_Definition (Parent (T));
+
+ if Nkind (Def) = N_Derived_Type_Definition then
+ Def := Record_Extension_Part (Def);
+ end if;
+
+ pragma Assert (Nkind (Def) = N_Record_Definition);
+ Comps := Component_List (Def);
+
+ if Present (Comps) then
+ Process_Component_List
+ (Comp_List => Comps,
+ CL_Checks => Checks);
+ end if;
+ end if;
+ end Add_Record_Component_Invariants;
+
+ -------------------------
+ -- Add_Type_Invariants --
+ -------------------------
+
+ procedure Add_Type_Invariants
+ (Priv_Typ : Entity_Id;
+ Full_Typ : Entity_Id;
+ CRec_Typ : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id;
+ Inherit : Boolean := False;
+ Priv_Item : Node_Id := Empty)
+ is
+ procedure Add_Invariant (Prag : Node_Id);
+ -- Create a runtime check to verify the invariant exression of pragma
+ -- Prag. All generated code is added to list Checks.
+
+ procedure Process_Type (T : Entity_Id; Stop_Item : Node_Id := Empty);
+ -- Generate invariant checks for type T by inspecting the rep item
+ -- chain of the type. Stop_Item denotes a rep item which once seen
+ -- will stop the inspection.
+
+ -------------------
+ -- Add_Invariant --
+ -------------------
+
+ procedure Add_Invariant (Prag : Node_Id) is
+ Rep_Typ : Entity_Id;
+ -- The replacement type used in the substitution of the current
+ -- instance of a type with the _object formal parameter.
+
+ procedure Replace_Type_Ref (N : Node_Id);
+ -- Substitute the occurrence of a type name denoted by N with a
+ -- reference to the _object formal parameter.
+
+ ----------------------
+ -- Replace_Type_Ref --
+ ----------------------
+
+ procedure Replace_Type_Ref (N : Node_Id) is
+ Nloc : constant Source_Ptr := Sloc (N);
+ Ref : Node_Id;
+
+ begin
+ -- Decorate the reference to Ref_Typ even though it may be
+ -- rewritten further down. This is done for two reasons:
+
+ -- 1) ASIS has all necessary semantic information in the
+ -- original tree.
+
+ -- 2) Routines which examine properties of the Original_Node
+ -- have some semantic information.
+
+ if Nkind (N) = N_Identifier then
+ Set_Entity (N, Rep_Typ);
+ Set_Etype (N, Rep_Typ);
+
+ elsif Nkind (N) = N_Selected_Component then
+ Analyze (Prefix (N));
+ Set_Entity (Selector_Name (N), Rep_Typ);
+ Set_Etype (Selector_Name (N), Rep_Typ);
+ end if;
+
+ -- Do not alter the tree for ASIS. As a result all references
+ -- to Ref_Typ remain as is, but they have sufficent semantic
+ -- information.
+
+ if not ASIS_Mode then
+
+ -- Perform the following substitution:
+
+ -- Ref_Typ --> _object
+
+ Ref := Make_Identifier (Nloc, Chars (Obj_Id));
+ Set_Entity (Ref, Obj_Id);
+ Set_Etype (Ref, Rep_Typ);
+
+ -- When the pragma denotes a class-wide invariant, perform
+ -- the following substitution:
+
+ -- Rep_Typ --> Rep_Typ'Class (_object)
+
+ if Class_Present (Prag) then
+ Ref :=
+ Make_Type_Conversion (Nloc,
+ Subtype_Mark =>
+ Make_Attribute_Reference (Nloc,
+ Prefix =>
+ New_Occurrence_Of (Rep_Typ, Nloc),
+ Attribute_Name => Name_Class),
+ Expression => Ref);
+ end if;
+
+ Rewrite (N, Ref);
+ Set_Comes_From_Source (N, True);
+ end if;
+ end Replace_Type_Ref;
+
+ procedure Replace_Type_Refs is
+ new Replace_Type_References_Generic (Replace_Type_Ref);
+
+ -- Local variables
+
+ Asp : constant Node_Id := Corresponding_Aspect (Prag);
+ Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
+ Ploc : constant Source_Ptr := Sloc (Prag);
+
+ Arg1 : Node_Id;
+ Arg2 : Node_Id;
+ Arg3 : Node_Id;
+ ASIS_Expr : Node_Id;
+ Assoc : List_Id;
+ Expr : Node_Id;
+ Str : String_Id;
+
+ -- Start of processing for Add_Invariant
+
+ begin
+ -- Nothing to do if the pragma was already processed
+
+ if Contains (Pragmas_Seen, Prag) then
+ return;
+ end if;
+
+ -- Extract the arguments of the invariant pragma
+
+ Arg1 := First (Pragma_Argument_Associations (Prag));
+ Arg2 := Next (Arg1);
+ Arg3 := Next (Arg2);
+
+ Arg1 := Get_Pragma_Arg (Arg1);
+ Arg2 := Get_Pragma_Arg (Arg2);
+
+ -- The pragma applies to the partial view
+
+ if Present (Priv_Typ) and then Entity (Arg1) = Priv_Typ then
+ Rep_Typ := Priv_Typ;
+
+ -- The pragma applies to the full view
+
+ elsif Present (Full_Typ) and then Entity (Arg1) = Full_Typ then
+ Rep_Typ := Full_Typ;
+
+ -- Otherwise the pragma applies to a parent type in which case it
+ -- will be processed at a later stage by Add_Parent_Invariants or
+ -- Add_Interface_Invariants.
+
+ else
+ return;
+ end if;
+
+ -- Nothing to do when the caller requests the processing of all
+ -- inherited class-wide invariants, but the pragma does not fall
+ -- in this category.
+
+ if Inherit and then not Class_Present (Prag) then
+ return;
+ end if;
+
+ Expr := New_Copy_Tree (Arg2);
+
+ -- Substitute all references to type Rep_Typ with references to
+ -- the _object formal parameter.
+
+ Replace_Type_Refs (Expr, Rep_Typ);
+
+ -- Additional processing for non-class-wide invariants
+
+ if not Inherit then
+
+ -- Preanalyze the invariant expression to detect errors and at
+ -- the same time capture the visibility of the proper package
+ -- part.
+
+ -- Historical note: the old implementation of invariants used
+ -- node N as the parent, but a package specification as parent
+ -- of an expression is bizarre.
+
+ Set_Parent (Expr, Parent (Arg2));
+ Preanalyze_Assert_Expression (Expr, Any_Boolean);
+
+ -- If the pragma comes from an aspect specification, replace
+ -- the saved expression because all type references must be
+ -- substituted for the call to Preanalyze_Spec_Expression in
+ -- Check_Aspect_At_xxx routines.
+
+ if Present (Asp) then
+ Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
+ end if;
+
+ -- Analyze the original invariant expression for ASIS
+
+ if ASIS_Mode then
+ ASIS_Expr := Empty;
+
+ if Comes_From_Source (Prag) then
+ ASIS_Expr := Arg2;
+ elsif Present (Asp) then
+ ASIS_Expr := Expression (Asp);
+ end if;
+
+ if Present (ASIS_Expr) then
+ Replace_Type_Refs (ASIS_Expr, Rep_Typ);
+ Preanalyze_Assert_Expression (ASIS_Expr, Any_Boolean);
+ end if;
+ end if;
+
+ -- A class-wide invariant may be inherited in a separate unit,
+ -- where the corresponding expression cannot be resolved by
+ -- visibility, because it refers to a local function. Propagate
+ -- semantic information to the original representation item, to
+ -- be used when an invariant procedure for a derived type is
+ -- constructed.
+
+ -- ??? Unclear how to handle class-wide invariants that are not
+ -- function calls.
+
+ if Class_Present (Prag)
+ and then Nkind (Expr) = N_Function_Call
+ and then Nkind (Arg2) = N_Indexed_Component
+ then
+ Rewrite (Arg2,
+ Make_Function_Call (Ploc,
+ Name =>
+ New_Occurrence_Of (Entity (Name (Expr)), Ploc),
+ Parameter_Associations => Expressions (Arg2)));
+ end if;
+ end if;
+
+ -- The invariant is ignored, nothing left to do
+
+ if Is_Ignored (Prag) then
+ null;
+
+ -- Otherwise the invariant is checked. Build a Check pragma to
+ -- verify the expression at runtime.
+
+ else
+ Assoc := New_List (
+ Make_Pragma_Argument_Association (Ploc,
+ Expression => Make_Identifier (Ploc, Nam)),
+ Make_Pragma_Argument_Association (Ploc,
+ Expression => Expr));
+
+ -- Handle the String argument (if any)
+
+ if Present (Arg3) then
+ Str := Strval (Get_Pragma_Arg (Arg3));
+
+ -- When inheriting an invariant, modify the message from
+ -- "failed invariant" to "failed inherited invariant".
+
+ if Inherit then
+ String_To_Name_Buffer (Str);
+
+ if Name_Buffer (1 .. 16) = "failed invariant" then
+ Insert_Str_In_Name_Buffer ("inherited ", 8);
+ Str := String_From_Name_Buffer;
+ end if;
+ end if;
+
+ Append_To (Assoc,
+ Make_Pragma_Argument_Association (Ploc,
+ Expression => Make_String_Literal (Ploc, Str)));
+ end if;
+
+ -- Generate:
+ -- pragma Check (<Nam>, <Expr>, <Str>);
+
+ Create_Append (Checks,
+ Make_Pragma (Ploc,
+ Pragma_Identifier =>
+ Make_Identifier (Ploc, Name_Check),
+ Pragma_Argument_Associations => Assoc));
+ end if;
+
+ -- Output an info message when inheriting an invariant and the
+ -- listing option is enabled.
+
+ if Inherit and Opt.List_Inherited_Aspects then
+ Error_Msg_Sloc := Sloc (Prag);
+ Error_Msg_N
+ ("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
+ end if;
+
+ -- Add the pragma to the list of processed pragmas
+
+ Append_New_Elmt (Prag, Pragmas_Seen);
+ Produced_Check := True;
+ end Add_Invariant;
+
+ ------------------
+ -- Process_Type --
+ ------------------
+
+ procedure Process_Type
+ (T : Entity_Id;
+ Stop_Item : Node_Id := Empty)
+ is
+ Rep_Item : Node_Id;
+
+ begin
+ Rep_Item := First_Rep_Item (T);
+ while Present (Rep_Item) loop
+ if Nkind (Rep_Item) = N_Pragma
+ and then Pragma_Name (Rep_Item) = Name_Invariant
+ then
+ -- Stop the traversal of the rep item chain once a specific
+ -- item is encountered.
+
+ if Present (Stop_Item) and then Rep_Item = Stop_Item then
+ exit;
+
+ -- Otherwise generate an invariant check
+
+ else
+ Add_Invariant (Rep_Item);
+ end if;
+ end if;
+
+ Next_Rep_Item (Rep_Item);
+ end loop;
+ end Process_Type;
+
+ -- Start of processing for Add_Type_Invariants
+
+ begin
+ -- Process the invariants of the partial view
+
+ if Present (Priv_Typ) then
+ Process_Type (Priv_Typ);
+ end if;
+
+ -- Process the invariants of the full view
+
+ if Present (Full_Typ) then
+ Process_Type (Full_Typ, Stop_Item => Priv_Item);
+
+ -- Process the elements of an array type
+
+ if Is_Array_Type (Full_Typ) then
+ Add_Array_Component_Invariants (Full_Typ, Obj_Id, Checks);
+
+ -- Process the components of a record type
+
+ elsif Ekind (Full_Typ) = E_Record_Type then
+ Add_Record_Component_Invariants (Full_Typ, Obj_Id, Checks);
+ end if;
+ end if;
+
+ -- Process the components of a corresponding record type
+
+ if Present (CRec_Typ) then
+ Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Checks);
+ end if;
+ end Add_Type_Invariants;
+
+ -------------------
+ -- Create_Append --
+ -------------------
+
+ procedure Create_Append (L : in out List_Id; N : Node_Id) is
+ begin
+ if No (L) then
+ L := New_List;
+ end if;
+
+ Append_To (L, N);
+ end Create_Append;
+
+ ------------------------------------
+ -- Is_Untagged_Private_Derivation --
+ ------------------------------------
+
+ function Is_Untagged_Private_Derivation
+ (Priv_Typ : Entity_Id;
+ Full_Typ : Entity_Id) return Boolean
+ is
+ begin
+ return
+ Present (Priv_Typ)
+ and then Is_Untagged_Derivation (Priv_Typ)
+ and then Is_Private_Type (Etype (Priv_Typ))
+ and then Present (Full_Typ)
+ and then Is_Itype (Full_Typ);
+ end Is_Untagged_Private_Derivation;
+
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
+ Dummy : Entity_Id;
+ Priv_Item : Node_Id;
+ Proc_Body : Node_Id;
+ Proc_Body_Id : Entity_Id;
+ Proc_Decl : Node_Id;
+ Proc_Id : Entity_Id;
+ Stmts : List_Id := No_List;
+
+ CRec_Typ : Entity_Id;
+ -- The corresponding record type of Full_Typ
+
+ Full_Proc : Entity_Id;
+ -- The entity of the "full" invariant procedure
+
+ Full_Typ : Entity_Id;
+ -- The full view of the working type
+
+ Freeze_Typ : Entity_Id;
+ -- The freeze type whose freeze node carries the invariant procedure
+ -- body. This is either the partial or the full view of the working
+ -- type.
+
+ Obj_Id : Entity_Id;
+ -- The _object formal parameter of the invariant procedure
+
+ Part_Proc : Entity_Id;
+ -- The entity of the "partial" invariant procedure
+
+ Priv_Typ : Entity_Id;
+ -- The partial view of the working type
+
+ Work_Typ : Entity_Id;
+ -- The working type
+
+ -- Start of processing for Build_Invariant_Procedure_Body
+
+ begin
+ Work_Typ := Typ;
+
+ -- The input type denotes the implementation base type of a constrained
+ -- array type. Work with the first subtype as all invariant pragmas are
+ -- on its rep item chain.
+
+ if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
+ Work_Typ := First_Subtype (Work_Typ);
+
+ -- The input type denotes the corresponding record type of a protected
+ -- or task type. Work with the concurrent type because the corresponding
+ -- record type may not be visible to clients of the type.
+
+ elsif Ekind (Work_Typ) = E_Record_Type
+ and then Is_Concurrent_Record_Type (Work_Typ)
+ then
+ Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
+ end if;
+
+ -- The type must either have invariants of its own, inherit class-wide
+ -- invariants from parent types or interfaces, or be an array or record
+ -- type whose components have invariants.
+
+ pragma Assert (Has_Invariants (Work_Typ));
+
+ -- Nothing to do for interface types as their class-wide invariants are
+ -- inherited by implementing types.
+
+ if Is_Interface (Work_Typ) then
+ return;
+ end if;
+
+ -- Obtain both views of the type
+
+ Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ);
+
+ -- The caller requests a body for the partial invariant procedure
+
+ if Partial_Invariant then
+ Full_Proc := Invariant_Procedure (Work_Typ);
+ Proc_Id := Partial_Invariant_Procedure (Work_Typ);
+
+ -- The "full" invariant procedure body was already created
+
+ if Present (Full_Proc)
+ and then Present
+ (Corresponding_Body (Unit_Declaration_Node (Full_Proc)))
+ then
+ -- This scenario happens only when the type is an untagged
+ -- derivation from a private parent and the underlying full
+ -- view was processed before the partial view.
+
+ pragma Assert
+ (Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ));
+
+ -- Nothing to do because the processing of the underlying full
+ -- view already checked the invariants of the partial view.
+
+ return;
+ end if;
+
+ -- Create a declaration for the "partial" invariant procedure if it
+ -- is not available.
+
+ if No (Proc_Id) then
+ Build_Invariant_Procedure_Declaration
+ (Typ => Work_Typ,
+ Partial_Invariant => True);
+
+ Proc_Id := Partial_Invariant_Procedure (Work_Typ);
+ end if;
+
+ -- The caller requests a body for the "full" invariant procedure
+
+ else
+ Proc_Id := Invariant_Procedure (Work_Typ);
+ Part_Proc := Partial_Invariant_Procedure (Work_Typ);
+
+ -- Create a declaration for the "full" invariant procedure if it is
+ -- not available.
+
+ if No (Proc_Id) then
+ Build_Invariant_Procedure_Declaration (Work_Typ);
+ Proc_Id := Invariant_Procedure (Work_Typ);
+ end if;
+ end if;
+
+ -- At this point there should be an invariant procedure declaration
+
+ pragma Assert (Present (Proc_Id));
+ Proc_Decl := Unit_Declaration_Node (Proc_Id);
+
+ -- Nothing to do if the invariant procedure already has a body
+
+ if Present (Corresponding_Body (Proc_Decl)) then
+ return;
+ end if;
+
+ -- The working type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the invariant procedure is properly marked as Ghost.
+
+ Set_Ghost_Mode_From_Entity (Work_Typ);
+
+ Obj_Id := First_Formal (Proc_Id);
+
+ -- The "partial" invariant procedure verifies the invariants of the
+ -- partial view only.
+
+ if Partial_Invariant then
+ pragma Assert (Present (Priv_Typ));
+ Freeze_Typ := Priv_Typ;
+
+ -- Emulate the environment of the invariant procedure by installing
+ -- its scope and formal parameters. Note that this is not need, but
+ -- having the scope of the invariant procedure installed helps with
+ -- the detection of invariant-related errors.
+
+ Push_Scope (Proc_Id);
+ Install_Formals (Proc_Id);
+
+ Add_Type_Invariants
+ (Priv_Typ => Priv_Typ,
+ Full_Typ => Empty,
+ CRec_Typ => Empty,
+ Obj_Id => Obj_Id,
+ Checks => Stmts);
+
+ End_Scope;
+
+ -- Otherwise the "full" invariant procedure verifies the invariants of
+ -- the full view, all array or record components, as well as class-wide
+ -- invariants inherited from parent types or interfaces. In addition, it
+ -- indirectly verifies the invariants of the partial view by calling the
+ -- "partial" invariant procedure.
+
+ else
+ pragma Assert (Present (Full_Typ));
+ Freeze_Typ := Full_Typ;
+
+ -- Check the invariants of the partial view by calling the "partial"
+ -- invariant procedure. Generate:
+
+ -- <Work_Typ>Partial_Invariant (_object);
+
+ if Present (Part_Proc) then
+ Create_Append (Stmts,
+ Make_Procedure_Call_Statement (Loc,
+ Name => New_Occurrence_Of (Part_Proc, Loc),
+ Parameter_Associations => New_List (
+ New_Occurrence_Of (Obj_Id, Loc))));
+
+ Produced_Check := True;
+ end if;
+
+ Priv_Item := Empty;
+
+ -- Derived subtypes do not have a partial view
+
+ if Present (Priv_Typ) then
+
+ -- The processing of the "full" invariant procedure intentionally
+ -- skips the partial view because a) this may result in changes of
+ -- visibility and b) lead to duplicate checks. However, when the
+ -- full view is the underlying full view of an untagged derived
+ -- type whose parent type is private, partial invariants appear on
+ -- the rep item chain of the partial view only.
+
+ -- package Pack_1 is
+ -- type Root ... is private;
+ -- private
+ -- <full view of Root>
+ -- end Pack_1;
+
+ -- with Pack_1;
+ -- package Pack_2 is
+ -- type Child is new Pack_1.Root with Type_Invariant => ...;
+ -- <underlying full view of Child>
+ -- end Pack_2;
+
+ -- As a result, the processing of the full view must also consider
+ -- all invariants of the partial view.
+
+ if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then
+ null;
+
+ -- Otherwise the invariants of the partial view are ignored
+
+ else
+ -- Note that the rep item chain is shared between the partial
+ -- and full views of a type. To avoid processing the invariants
+ -- of the partial view, signal the logic to stop when the first
+ -- rep item of the partial view has been reached.
+
+ Priv_Item := First_Rep_Item (Priv_Typ);
+
+ -- Ignore the invariants of the partial view by eliminating the
+ -- view.
+
+ Priv_Typ := Empty;
+ end if;
+ end if;
+
+ -- Process the invariants of the full view and in certain cases those
+ -- of the partial view. This also handles any invariants on array or
+ -- record components.
+
+ Add_Type_Invariants
+ (Priv_Typ => Priv_Typ,
+ Full_Typ => Full_Typ,
+ CRec_Typ => CRec_Typ,
+ Obj_Id => Obj_Id,
+ Checks => Stmts,
+ Priv_Item => Priv_Item);
+
+ -- Process the inherited class-wide invariants of all parent types.
+ -- This also handles any invariants on record components.
+
+ Add_Parent_Invariants (Full_Typ, Obj_Id, Stmts);
+
+ -- Process the inherited class-wide invariants of all implemented
+ -- interface types.
+
+ Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts);
+ end if;
+
+ -- At this point there should be at least one invariant check. If this
+ -- is not the case, then the invariant-related flags were not properly
+ -- set, or there is a missing invariant procedure on one of the array
+ -- or record components.
+
+ pragma Assert (Produced_Check);
+
+ -- Account for the case where assertions are disabled or all invariant
+ -- checks are subject to Assertion_Policy Ignore. Produce a completing
+ -- empty body.
+
+ if No (Stmts) then
+ Stmts := New_List (Make_Null_Statement (Loc));
+ end if;
+
+ Proc_Body :=
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Copy_Subprogram_Spec (Parent (Proc_Id)),
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Stmts));
+ Proc_Body_Id := Defining_Entity (Proc_Body);
+
+ -- Link both spec and body to avoid generating duplicates
+
+ Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
+ Set_Corresponding_Spec (Proc_Body, Proc_Id);
+
+ Append_Freeze_Action (Freeze_Typ, Proc_Body);
+ Ghost_Mode := Save_Ghost_Mode;
+ end Build_Invariant_Procedure_Body;
+
+ -------------------------------------------
+ -- Build_Invariant_Procedure_Declaration --
+ -------------------------------------------
+
+ procedure Build_Invariant_Procedure_Declaration
+ (Typ : Entity_Id;
+ Partial_Invariant : Boolean := False)
+ is
+ Loc : constant Source_Ptr := Sloc (Typ);
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
+ Proc_Id : Entity_Id;
+ Typ_Decl : Node_Id;
+
+ CRec_Typ : Entity_Id;
+ -- The corresponding record type of Full_Typ
+
+ Full_Base : Entity_Id;
+ -- The base type of Full_Typ
+
+ Full_Typ : Entity_Id;
+ -- The full view of working type
+
+ Obj_Id : Entity_Id;
+ -- The _object formal parameter of the invariant procedure
+
+ Priv_Typ : Entity_Id;
+ -- The partial view of working type
+
+ Work_Typ : Entity_Id;
+ -- The working type
+
+ begin
+ Work_Typ := Typ;
+
+ -- The input type denotes the implementation base type of a constrained
+ -- array type. Work with the first subtype as all invariant pragmas are
+ -- on its rep item chain.
+
+ if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
+ Work_Typ := First_Subtype (Work_Typ);
+
+ -- The input denotes the corresponding record type of a protected or a
+ -- task type. Work with the concurrent type because the corresponding
+ -- record type may not be visible to clients of the type.
+
+ elsif Ekind (Work_Typ) = E_Record_Type
+ and then Is_Concurrent_Record_Type (Work_Typ)
+ then
+ Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
+ end if;
+
+ -- The type must either have invariants of its own, inherit class-wide
+ -- invariants from parent or interface types, or be an array or record
+ -- type whose components have invariants.
+
+ pragma Assert (Has_Invariants (Work_Typ));
+
+ -- Nothing to do for interface types as their class-wide invariants are
+ -- inherited by implementing types.
+
+ if Is_Interface (Work_Typ) then
+ return;
+
+ -- Nothing to do if the type already has a "partial" invariant procedure
+
+ elsif Partial_Invariant then
+ if Present (Partial_Invariant_Procedure (Work_Typ)) then
+ return;
+ end if;
+
+ -- Nothing to do if the type already has a "full" invariant procedure
+
+ elsif Present (Invariant_Procedure (Work_Typ)) then
+ return;
+ end if;
+
+ -- The working type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the invariant procedure is properly marked as Ghost.
+
+ Set_Ghost_Mode_From_Entity (Work_Typ);
+
+ -- The caller requests the declaration of the "partial" invariant
+ -- procedure.
+
+ if Partial_Invariant then
+ Proc_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars =>
+ New_External_Name (Chars (Work_Typ), "Partial_Invariant"));
+
+ Set_Ekind (Proc_Id, E_Procedure);
+ Set_Is_Partial_Invariant_Procedure (Proc_Id);
+ Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id);
+
+ -- Otherwise the caller requests the declaration of the "full" invariant
+ -- procedure.
+
+ else
+ Proc_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Work_Typ), "Invariant"));
+
+ Set_Ekind (Proc_Id, E_Procedure);
+ Set_Is_Invariant_Procedure (Proc_Id);
+ Set_Invariant_Procedure (Work_Typ, Proc_Id);
+ end if;
+
+ -- The invariant procedure requires debug info when the invariants are
+ -- subject to Source Coverage Obligations.
+
+ if Opt.Generate_SCO then
+ Set_Needs_Debug_Info (Proc_Id);
+ end if;
+
+ -- Mark the invariant procedure explicitly as Ghost because it does not
+ -- come from source.
+
+ if Ghost_Mode > None then
+ Set_Is_Ghost_Entity (Proc_Id);
+ end if;
+
+ -- Obtain all views of the input type
+
+ Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
+
+ -- Associate the invariant procedure with all views
+
+ Propagate_Invariant_Attributes (Priv_Typ, From_Typ => Work_Typ);
+ Propagate_Invariant_Attributes (Full_Typ, From_Typ => Work_Typ);
+ Propagate_Invariant_Attributes (Full_Base, From_Typ => Work_Typ);
+ Propagate_Invariant_Attributes (CRec_Typ, From_Typ => Work_Typ);
+
+ -- The declaration of the invariant procedure is inserted after the
+ -- declaration of the partial view as this allows for proper external
+ -- visibility.
+
+ if Present (Priv_Typ) then
+ Typ_Decl := Declaration_Node (Priv_Typ);
+
+ -- Derived types with the full view as parent do not have a partial
+ -- view. Insert the invariant procedure after the derived type.
+
+ else
+ Typ_Decl := Declaration_Node (Full_Typ);
+ end if;
+
+ -- The type should have a declarative node
+
+ pragma Assert (Present (Typ_Decl));
+
+ -- Create the formal parameter which emulates the variable-like behavior
+ -- of the current type instance.
+
+ Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject);
+ Set_Ekind (Obj_Id, E_In_Parameter);
+
+ -- Generate:
+ -- procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>);
+
+ Insert_After_And_Analyze (Typ_Decl,
+ Make_Subprogram_Declaration (Loc,
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Proc_Id,
+ Parameter_Specifications => New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Obj_Id,
+ Parameter_Type =>
+ New_Occurrence_Of (Work_Typ, Loc))))));
+
+ Ghost_Mode := Save_Ghost_Mode;
+ end Build_Invariant_Procedure_Declaration;
+
---------------------
-- Build_Late_Proc --
---------------------
===================================================================
@@ -118,9 +118,24 @@
-- finalization master must be analyzed. Insertion_Node is the insertion
-- point before which the master is to be inserted.
+ procedure Build_Invariant_Procedure_Body
+ (Typ : Entity_Id;
+ Partial_Invariant : Boolean := False);
+ -- Create the body of the procedure which verifies the invariants of type
+ -- Typ at runtime. Flag Partial_Invariant should be set when Typ denotes a
+ -- private type, otherwise it is assumed that Typ denotes the full view of
+ -- a private type.
+
+ procedure Build_Invariant_Procedure_Declaration
+ (Typ : Entity_Id;
+ Partial_Invariant : Boolean := False);
+ -- Create the declaration of the procedure which verifies the invariants of
+ -- type Typ at runtime. Flag Partial_Invariant should be set when building
+ -- the invariant procedure for a private type.
+
procedure Build_Late_Proc (Typ : Entity_Id; Nam : Name_Id);
- -- Build one controlling procedure when a late body overrides one of
- -- the controlling operations.
+ -- Build one controlling procedure when a late body overrides one of the
+ -- controlling operations.
procedure Build_Object_Declarations
(Data : out Finalization_Exception_Data;
===================================================================
@@ -6405,30 +6405,19 @@
-------------------------
function Make_Invariant_Call (Expr : Node_Id) return Node_Id is
- Loc : constant Source_Ptr := Sloc (Expr);
- Typ : Entity_Id;
+ Loc : constant Source_Ptr := Sloc (Expr);
+ Typ : constant Entity_Id := Base_Type (Etype (Expr));
+ Proc_Id : Entity_Id;
begin
- Typ := Etype (Expr);
+ pragma Assert (Has_Invariants (Typ));
- -- Subtypes may be subject to invariants coming from their respective
- -- base types. The subtype may be fully or partially private.
+ Proc_Id := Invariant_Procedure (Typ);
+ pragma Assert (Present (Proc_Id));
- if Ekind_In (Typ, E_Array_Subtype,
- E_Private_Subtype,
- E_Record_Subtype,
- E_Record_Subtype_With_Private)
- then
- Typ := Base_Type (Typ);
- end if;
-
- pragma Assert
- (Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)));
-
return
Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of (Invariant_Procedure (Typ), Loc),
+ Name => New_Occurrence_Of (Proc_Id, Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
end Make_Invariant_Call;
===================================================================
@@ -1526,12 +1526,6 @@
Set_Stored_Constraint (Rec_Ent, No_Elist);
Cdecls := New_List;
- -- Propagate type invariants to the corresponding record type
-
- Set_Has_Invariants (Rec_Ent, Has_Invariants (Ctyp));
- Set_Has_Inheritable_Invariants (Rec_Ent,
- Has_Inheritable_Invariants (Ctyp));
-
-- Use discriminals to create list of discriminants for record, and
-- create new discriminals for use in default expressions, etc. It is
-- worth noting that a task discriminant gives rise to 5 entities;
===================================================================
@@ -35,6 +35,7 @@
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
+with Exp_Ch7; use Exp_Ch7;
with Exp_Disp; use Exp_Disp;
with Exp_Dist; use Exp_Dist;
with Exp_Dbug; use Exp_Dbug;
@@ -1457,15 +1458,17 @@
Inherit_Default_Init_Cond_Procedure (E);
end if;
- -- If invariants are present, build the invariant procedure for a
- -- private type, but not any of its subtypes or interface types.
+ -- Preanalyze and resolve the invariants of a private type at the
+ -- end of the visible declarations to catch potential errors. Note
+ -- that inherited class-wide invariants are not considered because
+ -- they have already been resolved.
- if Has_Invariants (E) then
- if Ekind (E) = E_Private_Subtype then
- null;
- else
- Build_Invariant_Procedure (E, N);
- end if;
+ if Ekind_In (E, E_Limited_Private_Type,
+ E_Private_Type,
+ E_Record_Type_With_Private)
+ and then Has_Own_Invariants (E)
+ then
+ Build_Invariant_Procedure_Body (E, Partial_Invariant => True);
end if;
end if;
@@ -1473,7 +1476,7 @@
end loop;
if Is_Remote_Call_Interface (Id)
- and then Nkind (Parent (Parent (N))) = N_Compilation_Unit
+ and then Nkind (Parent (Parent (N))) = N_Compilation_Unit
then
Validate_RCI_Declarations (Id);
end if;
@@ -1544,7 +1547,6 @@
if Is_Compilation_Unit (Id) then
Install_Private_With_Clauses (Id);
else
-
-- The current compilation unit may include private with_clauses,
-- which are visible in the private part of the current nested
-- package, and have to be installed now. This is not done for
@@ -1636,48 +1638,18 @@
("full view of & does not have preelaborable initialization", E);
end if;
- -- An invariant may appear on a full view of a type
+ -- Preanalyze and resolve the invariants of a private type's full
+ -- view at the end of the private declarations in case freezing did
+ -- not take place either due to errors or because the context is a
+ -- generic unit.
if Is_Type (E)
+ and then not Is_Private_Type (E)
and then Has_Private_Declaration (E)
- and then Nkind (Parent (E)) = N_Full_Type_Declaration
+ and then Has_Invariants (E)
+ and then Serious_Errors_Detected > 0
then
- declare
- IP_Built : Boolean := False;
-
- begin
- if Has_Aspects (Parent (E)) then
- declare
- ASN : Node_Id;
-
- begin
- ASN := First (Aspect_Specifications (Parent (E)));
- while Present (ASN) loop
- if Nam_In (Chars (Identifier (ASN)),
- Name_Invariant,
- Name_Type_Invariant)
- then
- Build_Invariant_Procedure (E, N);
- IP_Built := True;
- exit;
- end if;
-
- Next (ASN);
- end loop;
- end;
- end if;
-
- -- Invariants may have been inherited from progenitors
-
- if not IP_Built
- and then Has_Interfaces (E)
- and then Has_Inheritable_Invariants (E)
- and then not Is_Interface (E)
- and then not Is_Class_Wide_Type (E)
- then
- Build_Invariant_Procedure (E, N);
- end if;
- end;
+ Build_Invariant_Procedure_Body (E);
end if;
Next_Entity (E);
@@ -2543,7 +2515,7 @@
Priv_Elmt : Elmt_Id;
Priv_Sub : Entity_Id;
- procedure Preserve_Full_Attributes (Priv, Full : Entity_Id);
+ procedure Preserve_Full_Attributes (Priv : Entity_Id; Full : Entity_Id);
-- Copy to the private declaration the attributes of the full view that
-- need to be available for the partial view also.
@@ -2554,12 +2526,16 @@
-- Preserve_Full_Attributes --
------------------------------
- procedure Preserve_Full_Attributes (Priv, Full : Entity_Id) is
- Priv_Is_Base_Type : constant Boolean := Is_Base_Type (Priv);
+ procedure Preserve_Full_Attributes
+ (Priv : Entity_Id;
+ Full : Entity_Id)
+ is
+ Full_Base : constant Entity_Id := Base_Type (Full);
+ Priv_Is_Base_Type : constant Boolean := Is_Base_Type (Priv);
begin
- Set_Size_Info (Priv, (Full));
- Set_RM_Size (Priv, RM_Size (Full));
+ Set_Size_Info (Priv, Full);
+ Set_RM_Size (Priv, RM_Size (Full));
Set_Size_Known_At_Compile_Time
(Priv, Size_Known_At_Compile_Time (Full));
Set_Is_Volatile (Priv, Is_Volatile (Full));
@@ -2581,27 +2557,31 @@
end if;
if Priv_Is_Base_Type then
- Set_Is_Controlled (Priv, Is_Controlled (Base_Type (Full)));
+ Set_Is_Controlled (Priv, Is_Controlled (Full_Base));
Set_Finalize_Storage_Only
- (Priv, Finalize_Storage_Only
- (Base_Type (Full)));
- Propagate_Concurrent_Flags
- (Priv, Base_Type (Full));
+ (Priv, Finalize_Storage_Only (Full_Base));
Set_Has_Controlled_Component
- (Priv, Has_Controlled_Component
- (Base_Type (Full)));
+ (Priv, Has_Controlled_Component (Full_Base));
+
+ Propagate_Concurrent_Flags (Priv, Base_Type (Full));
end if;
Set_Freeze_Node (Priv, Freeze_Node (Full));
- -- Propagate information of type invariants, which may be specified
- -- for the full view.
+ -- Propagate invariant-related attributes from the base type of the
+ -- full view to the full view and vice versa. This may seem strange,
+ -- but is necessary depending on which type triggered the generation
+ -- of the invariant procedure body. As a result, both the full view
+ -- and its base type carry the same invariant-related information.
- 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;
+ Propagate_Invariant_Attributes (Full, From_Typ => Full_Base);
+ Propagate_Invariant_Attributes (Full_Base, From_Typ => Full);
+ -- Propagate invariant-related attributes from the full view to the
+ -- private view.
+
+ Propagate_Invariant_Attributes (Priv, From_Typ => Full);
+
if Is_Tagged_Type (Priv)
and then Is_Tagged_Type (Full)
and then not Error_Posted (Full)
@@ -2943,7 +2923,7 @@
if Is_Overloadable (Subp) and then Is_Primitive (Subp) then
Error_Msg_NE
("type& must be completed in the private part",
- Parent (Subp), Id);
+ Parent (Subp), Id);
-- The result type of an access-to-function type cannot be a
-- Taft-amendment type, unless the version is Ada 2012 or
===================================================================
@@ -2037,11 +2037,21 @@
Set_Is_Constrained (T, not Has_Discriminants (T));
- -- If aspects are present, analyze them now. They can make references
- -- to the discriminants of the type, but not to any components.
+ -- If aspects are present, analyze them now. They can make references to
+ -- the discriminants of the type, but not to any components.
if Has_Aspects (N) then
- Analyze_Aspect_Specifications (N, Def_Id);
+
+ -- The protected type is the full view of a private type. Analyze the
+ -- aspects with the entity of the private type to ensure that after
+ -- both views are exchanged, the aspect are actually associated with
+ -- the full view.
+
+ if T /= Def_Id and then Is_Private_Type (Def_Id) then
+ Analyze_Aspect_Specifications (N, T);
+ else
+ Analyze_Aspect_Specifications (N, Def_Id);
+ end if;
end if;
Analyze (Protected_Definition (N));
@@ -2194,6 +2204,11 @@
Set_Must_Have_Preelab_Init (T);
end if;
+ -- Propagate invariant-related attributes from the private type to
+ -- the protected type.
+
+ Propagate_Invariant_Attributes (T, From_Typ => Def_Id);
+
-- Create corresponding record now, because some private dependents
-- may be subtypes of the partial view.
@@ -3071,7 +3086,17 @@
Set_Is_Constrained (T, not Has_Discriminants (T));
if Has_Aspects (N) then
- Analyze_Aspect_Specifications (N, Def_Id);
+
+ -- The task type is the full view of a private type. Analyze the
+ -- aspects with the entity of the private type to ensure that after
+ -- both views are exchanged, the aspect are actually associated with
+ -- the full view.
+
+ if T /= Def_Id and then Is_Private_Type (Def_Id) then
+ Analyze_Aspect_Specifications (N, T);
+ else
+ Analyze_Aspect_Specifications (N, Def_Id);
+ end if;
end if;
if Present (Task_Definition (N)) then
@@ -3102,9 +3127,8 @@
-- Case of a completion of a private declaration
- if T /= Def_Id
- and then Is_Private_Type (Def_Id)
- then
+ if T /= Def_Id and then Is_Private_Type (Def_Id) then
+
-- Deal with preelaborable initialization. Note that this processing
-- is done by Process_Full_View, but as can be seen below, in this
-- case the call to Process_Full_View is skipped if any serious
@@ -3114,6 +3138,11 @@
Set_Must_Have_Preelab_Init (T);
end if;
+ -- Propagate invariant-related attributes from the private type to
+ -- task type.
+
+ Propagate_Invariant_Attributes (T, From_Typ => Def_Id);
+
-- Create corresponding record now, because some private dependents
-- may be subtypes of the partial view.
===================================================================
@@ -245,7 +245,7 @@
-- Underlying_Record_View Node28
-- BIP_Initialization_Call Node29
- -- Subprograms_For_Type Node29
+ -- Subprograms_For_Type Elist29
-- Anonymous_Object Node30
-- Corresponding_Equality Node30
@@ -539,7 +539,7 @@
-- Has_Pragma_Inline_Always Flag230
-- Renamed_In_Spec Flag231
- -- Has_Invariants Flag232
+ -- Has_Own_Invariants Flag232
-- Has_Pragma_Unmodified Flag233
-- Is_Dispatch_Table_Entity Flag234
-- Is_Trivial_Subprogram Flag235
@@ -603,10 +603,11 @@
-- Predicates_Ignored Flag288
-- Has_Timing_Event Flag289
- -- (unused) Flag290
+ -- (unused) Flag290 -- ??? flag breaks einfo.h
- -- (unused) Flag291
- -- (unused) Flag292
+ -- Has_Inherited_Invariants Flag291
+ -- Is_Partial_Invariant_Procedure Flag292
+
-- (unused) Flag293
-- (unused) Flag294
-- (unused) Flag295
@@ -614,8 +615,8 @@
-- (unused) Flag297
-- (unused) Flag298
-- (unused) Flag299
+ -- (unused) Flag300
- -- (unused) Flag300
-- (unused) Flag301
-- (unused) Flag302
-- (unused) Flag303
@@ -1610,18 +1611,18 @@
return Flag133 (Base_Type (Id));
end Has_Inherited_Default_Init_Cond;
+ function Has_Inherited_Invariants (Id : E) return B is
+ begin
+ pragma Assert (Is_Type (Id));
+ return Flag291 (Id);
+ end Has_Inherited_Invariants;
+
function Has_Initial_Value (Id : E) return B is
begin
pragma Assert (Ekind (Id) = E_Variable or else Is_Formal (Id));
return Flag219 (Id);
end Has_Initial_Value;
- function Has_Invariants (Id : E) return B is
- begin
- pragma Assert (Is_Type (Id));
- return Flag232 (Id);
- end Has_Invariants;
-
function Has_Loop_Entry_Attributes (Id : E) return B is
begin
pragma Assert (Ekind (Id) = E_Loop);
@@ -1675,6 +1676,12 @@
return Flag110 (Id);
end Has_Out_Or_In_Out_Parameter;
+ function Has_Own_Invariants (Id : E) return B is
+ begin
+ pragma Assert (Is_Type (Id));
+ return Flag232 (Id);
+ end Has_Own_Invariants;
+
function Has_Per_Object_Constraint (Id : E) return B is
begin
return Flag154 (Id);
@@ -2388,6 +2395,12 @@
return Flag215 (Base_Type (Id));
end Is_Param_Block_Component_Type;
+ function Is_Partial_Invariant_Procedure (Id : E) return B is
+ begin
+ pragma Assert (Ekind_In (Id, E_Function, E_Procedure));
+ return Flag292 (Id);
+ end Is_Partial_Invariant_Procedure;
+
function Is_Potentially_Use_Visible (Id : E) return B is
begin
pragma Assert (Nkind (Id) in N_Entity);
@@ -3314,10 +3327,10 @@
return Node18 (Id);
end String_Literal_Low_Bound;
- function Subprograms_For_Type (Id : E) return E is
+ function Subprograms_For_Type (Id : E) return L is
begin
- pragma Assert (Is_Type (Id) or else Is_Subprogram (Id));
- return Node29 (Id);
+ pragma Assert (Is_Type (Id));
+ return Elist29 (Id);
end Subprograms_For_Type;
function Subps_Index (Id : E) return U is
@@ -4596,18 +4609,18 @@
Set_Flag133 (Base_Type (Id), V);
end Set_Has_Inherited_Default_Init_Cond;
+ procedure Set_Has_Inherited_Invariants (Id : E; V : B := True) is
+ begin
+ pragma Assert (Is_Type (Id));
+ Set_Flag291 (Id, V);
+ end Set_Has_Inherited_Invariants;
+
procedure Set_Has_Initial_Value (Id : E; V : B := True) is
begin
pragma Assert (Ekind_In (Id, E_Variable, E_Out_Parameter));
Set_Flag219 (Id, V);
end Set_Has_Initial_Value;
- procedure Set_Has_Invariants (Id : E; V : B := True) is
- begin
- pragma Assert (Is_Type (Id));
- Set_Flag232 (Id, V);
- end Set_Has_Invariants;
-
procedure Set_Has_Loop_Entry_Attributes (Id : E; V : B := True) is
begin
pragma Assert (Ekind (Id) = E_Loop);
@@ -4662,6 +4675,12 @@
Set_Flag110 (Id, V);
end Set_Has_Out_Or_In_Out_Parameter;
+ procedure Set_Has_Own_Invariants (Id : E; V : B := True) is
+ begin
+ pragma Assert (Is_Type (Id));
+ Set_Flag232 (Id, V);
+ end Set_Has_Own_Invariants;
+
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True) is
begin
Set_Flag154 (Id, V);
@@ -5442,6 +5461,12 @@
Set_Flag215 (Id, V);
end Set_Is_Param_Block_Component_Type;
+ procedure Set_Is_Partial_Invariant_Procedure (Id : E; V : B := True) is
+ begin
+ pragma Assert (Ekind (Id) = E_Procedure);
+ Set_Flag292 (Id, V);
+ end Set_Is_Partial_Invariant_Procedure;
+
procedure Set_Is_Potentially_Use_Visible (Id : E; V : B := True) is
begin
pragma Assert (Nkind (Id) in N_Entity);
@@ -5450,7 +5475,7 @@
procedure Set_Is_Predicate_Function (Id : E; V : B := True) is
begin
- pragma Assert (Ekind_In (Id, E_Function, E_Procedure));
+ pragma Assert (Ekind (Id) = E_Function);
Set_Flag255 (Id, V);
end Set_Is_Predicate_Function;
@@ -6404,10 +6429,10 @@
Set_Node18 (Id, V);
end Set_String_Literal_Low_Bound;
- procedure Set_Subprograms_For_Type (Id : E; V : E) is
+ procedure Set_Subprograms_For_Type (Id : E; V : L) is
begin
- pragma Assert (Is_Type (Id) or else Is_Subprogram (Id));
- Set_Node29 (Id, V);
+ pragma Assert (Is_Type (Id));
+ Set_Elist29 (Id, V);
end Set_Subprograms_For_Type;
procedure Set_Subps_Index (Id : E; V : U) is
@@ -6945,23 +6970,31 @@
---------------------------------
function Default_Init_Cond_Procedure (Id : E) return E is
- Subp_Id : Entity_Id;
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
begin
pragma Assert
(Is_Type (Id)
and then (Has_Default_Init_Cond (Id)
- or Has_Inherited_Default_Init_Cond (Id)));
+ or else Has_Inherited_Default_Init_Cond (Id)));
- Subp_Id := Subprograms_For_Type (Base_Type (Id));
- while Present (Subp_Id) loop
- if Is_Default_Init_Cond_Procedure (Subp_Id) then
- return Subp_Id;
- end if;
+ Subps := Subprograms_For_Type (Base_Type (Id));
- Subp_Id := Subprograms_For_Type (Subp_Id);
- end loop;
+ if Present (Subps) then
+ Subp_Elmt := First_Elmt (Subps);
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+ if Is_Default_Init_Cond_Procedure (Subp_Id) then
+ return Subp_Id;
+ end if;
+
+ Next_Elmt (Subp_Elmt);
+ end loop;
+ end if;
+
return Empty;
end Default_Init_Cond_Procedure;
@@ -7370,6 +7403,15 @@
return False;
end Has_Interrupt_Handler;
+ --------------------
+ -- Has_Invariants --
+ --------------------
+
+ function Has_Invariants (Id : E) return B is
+ begin
+ return Has_Own_Invariants (Id) or else Has_Inherited_Invariants (Id);
+ end Has_Invariants;
+
--------------------------
-- Has_Non_Limited_View --
--------------------------
@@ -7533,26 +7575,29 @@
-------------------------
function Invariant_Procedure (Id : E) return E is
- S : Entity_Id;
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
begin
- pragma Assert (Is_Type (Id) and then Has_Invariants (Id));
+ pragma Assert (Is_Type (Id));
- if No (Subprograms_For_Type (Id)) then
- return Empty;
+ Subps := Subprograms_For_Type (Id);
- else
- S := Subprograms_For_Type (Id);
- while Present (S) loop
- if Is_Invariant_Procedure (S) then
- return S;
- else
- S := Subprograms_For_Type (S);
+ if Present (Subps) then
+ Subp_Elmt := First_Elmt (Subps);
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Is_Invariant_Procedure (Subp_Id) then
+ return Subp_Id;
end if;
+
+ Next_Elmt (Subp_Elmt);
end loop;
+ end if;
- return Empty;
- end if;
+ return Empty;
end Invariant_Procedure;
----------------------
@@ -8261,46 +8306,81 @@
return Ekind (Id);
end Parameter_Mode;
+ ---------------------------------
+ -- Partial_Invariant_Procedure --
+ ---------------------------------
+
+ function Partial_Invariant_Procedure (Id : E) return E is
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
+
+ begin
+ pragma Assert (Is_Type (Id));
+
+ Subps := Subprograms_For_Type (Id);
+
+ if Present (Subps) then
+ Subp_Elmt := First_Elmt (Subps);
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Is_Partial_Invariant_Procedure (Subp_Id) then
+ return Subp_Id;
+ end if;
+
+ Next_Elmt (Subp_Elmt);
+ end loop;
+ end if;
+
+ return Empty;
+ end Partial_Invariant_Procedure;
+
------------------------
-- Predicate_Function --
------------------------
function Predicate_Function (Id : E) return E is
- S : Entity_Id;
- T : Entity_Id;
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
+ Typ : Entity_Id;
begin
pragma Assert (Is_Type (Id));
- -- If type is private and has a completion, predicate may be defined
- -- on the full view.
+ -- If type is private and has a completion, predicate may be defined on
+ -- the full view.
if Is_Private_Type (Id)
and then
(not Has_Predicates (Id) or else No (Subprograms_For_Type (Id)))
and then Present (Full_View (Id))
then
- T := Full_View (Id);
+ Typ := Full_View (Id);
else
- T := Id;
+ Typ := Id;
end if;
- if No (Subprograms_For_Type (T)) then
- return Empty;
+ Subps := Subprograms_For_Type (Typ);
- else
- S := Subprograms_For_Type (T);
- while Present (S) loop
- if Is_Predicate_Function (S) then
- return S;
- else
- S := Subprograms_For_Type (S);
+ if Present (Subps) then
+ Subp_Elmt := First_Elmt (Subps);
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Ekind (Subp_Id) = E_Function
+ and then Is_Predicate_Function (Subp_Id)
+ then
+ return Subp_Id;
end if;
+
+ Next_Elmt (Subp_Elmt);
end loop;
+ end if;
- return Empty;
- end if;
+ return Empty;
end Predicate_Function;
--------------------------
@@ -8308,36 +8388,46 @@
--------------------------
function Predicate_Function_M (Id : E) return E is
- S : Entity_Id;
- T : Entity_Id;
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
+ Typ : Entity_Id;
begin
pragma Assert (Is_Type (Id));
- -- If type is private and has a completion, predicate may be defined
- -- on the full view.
+ -- If type is private and has a completion, predicate may be defined on
+ -- the full view.
- if Is_Private_Type (Id) and then Present (Full_View (Id)) then
- T := Full_View (Id);
+ if Is_Private_Type (Id)
+ and then
+ (not Has_Predicates (Id) or else No (Subprograms_For_Type (Id)))
+ and then Present (Full_View (Id))
+ then
+ Typ := Full_View (Id);
+
else
- T := Id;
+ Typ := Id;
end if;
- if No (Subprograms_For_Type (T)) then
- return Empty;
+ Subps := Subprograms_For_Type (Typ);
- else
- S := Subprograms_For_Type (T);
- while Present (S) loop
- if Is_Predicate_Function_M (S) then
- return S;
- else
- S := Subprograms_For_Type (S);
+ if Present (Subps) then
+ Subp_Elmt := First_Elmt (Subps);
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Ekind (Subp_Id) = E_Function
+ and then Is_Predicate_Function_M (Subp_Id)
+ then
+ return Subp_Id;
end if;
+
+ Next_Elmt (Subp_Elmt);
end loop;
+ end if;
- return Empty;
- end if;
+ return Empty;
end Predicate_Function_M;
-------------------------
@@ -8563,8 +8653,10 @@
-------------------------------------
procedure Set_Default_Init_Cond_Procedure (Id : E; V : E) is
- Base_Typ : Entity_Id;
- Subp_Id : Entity_Id;
+ Base_Typ : Entity_Id;
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
begin
-- Once set, this attribute cannot be reset
@@ -8577,21 +8669,29 @@
pragma Assert
(Is_Type (Id)
and then (Has_Default_Init_Cond (Id)
- or Has_Inherited_Default_Init_Cond (Id)));
+ or else Has_Inherited_Default_Init_Cond (Id)));
+
Base_Typ := Base_Type (Id);
+ Subps := Subprograms_For_Type (Base_Typ);
- Subp_Id := Subprograms_For_Type (Base_Typ);
- Set_Subprograms_For_Type (Base_Typ, V);
- Set_Subprograms_For_Type (V, Subp_Id);
+ if No (Subps) then
+ Subps := New_Elmt_List;
+ Set_Subprograms_For_Type (Base_Typ, Subps);
+ end if;
- -- Check for a duplicate procedure
+ Subp_Elmt := First_Elmt (Subps);
+ Prepend_Elmt (V, Subps);
- while Present (Subp_Id) loop
+ -- Check for a duplicate default initial condition procedure
+
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
if Is_Default_Init_Cond_Procedure (Subp_Id) then
raise Program_Error;
end if;
- Subp_Id := Subprograms_For_Type (Subp_Id);
+ Next_Elmt (Subp_Elmt);
end loop;
end Set_Default_Init_Cond_Procedure;
@@ -8600,46 +8700,105 @@
-----------------------------
procedure Set_Invariant_Procedure (Id : E; V : E) is
- S : Entity_Id;
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
begin
- pragma Assert (Is_Type (Id) and then Has_Invariants (Id));
+ pragma Assert (Is_Type (Id));
- S := Subprograms_For_Type (Id);
- Set_Subprograms_For_Type (Id, V);
- Set_Subprograms_For_Type (V, S);
+ Subps := Subprograms_For_Type (Id);
- -- Check for duplicate entry
+ if No (Subps) then
+ Subps := New_Elmt_List;
+ Set_Subprograms_For_Type (Id, Subps);
+ end if;
- while Present (S) loop
- if Is_Invariant_Procedure (S) then
+ Subp_Elmt := First_Elmt (Subps);
+ Prepend_Elmt (V, Subps);
+
+ -- Check for a duplicate invariant procedure
+
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Is_Invariant_Procedure (Subp_Id) then
raise Program_Error;
- else
- S := Subprograms_For_Type (S);
end if;
+
+ Next_Elmt (Subp_Elmt);
end loop;
end Set_Invariant_Procedure;
+ -------------------------------------
+ -- Set_Partial_Invariant_Procedure --
+ -------------------------------------
+
+ procedure Set_Partial_Invariant_Procedure (Id : E; V : E) is
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
+
+ begin
+ pragma Assert (Is_Type (Id));
+
+ Subps := Subprograms_For_Type (Id);
+
+ if No (Subps) then
+ Subps := New_Elmt_List;
+ Set_Subprograms_For_Type (Id, Subps);
+ end if;
+
+ Subp_Elmt := First_Elmt (Subps);
+ Prepend_Elmt (V, Subps);
+
+ -- Check for a duplicate partial invariant procedure
+
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Is_Partial_Invariant_Procedure (Subp_Id) then
+ raise Program_Error;
+ end if;
+
+ Next_Elmt (Subp_Elmt);
+ end loop;
+ end Set_Partial_Invariant_Procedure;
+
----------------------------
-- Set_Predicate_Function --
----------------------------
procedure Set_Predicate_Function (Id : E; V : E) is
- S : Entity_Id;
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
begin
pragma Assert (Is_Type (Id) and then Has_Predicates (Id));
- S := Subprograms_For_Type (Id);
- Set_Subprograms_For_Type (Id, V);
- Set_Subprograms_For_Type (V, S);
+ Subps := Subprograms_For_Type (Id);
- while Present (S) loop
- if Is_Predicate_Function (S) then
+ if No (Subps) then
+ Subps := New_Elmt_List;
+ Set_Subprograms_For_Type (Id, Subps);
+ end if;
+
+ Subp_Elmt := First_Elmt (Subps);
+ Prepend_Elmt (V, Subps);
+
+ -- Check for a duplicate predication function
+
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Ekind (Subp_Id) = E_Function
+ and then Is_Predicate_Function (Subp_Id)
+ then
raise Program_Error;
- else
- S := Subprograms_For_Type (S);
end if;
+
+ Next_Elmt (Subp_Elmt);
end loop;
end Set_Predicate_Function;
@@ -8648,23 +8807,35 @@
------------------------------
procedure Set_Predicate_Function_M (Id : E; V : E) is
- S : Entity_Id;
+ Subp_Elmt : Elmt_Id;
+ Subp_Id : Entity_Id;
+ Subps : Elist_Id;
begin
pragma Assert (Is_Type (Id) and then Has_Predicates (Id));
- S := Subprograms_For_Type (Id);
- Set_Subprograms_For_Type (Id, V);
- Set_Subprograms_For_Type (V, S);
+ Subps := Subprograms_For_Type (Id);
- -- Check for duplicates
+ if No (Subps) then
+ Subps := New_Elmt_List;
+ Set_Subprograms_For_Type (Id, Subps);
+ end if;
- while Present (S) loop
- if Is_Predicate_Function_M (S) then
+ Subp_Elmt := First_Elmt (Subps);
+ Prepend_Elmt (V, Subps);
+
+ -- Check for a duplicate predication function
+
+ while Present (Subp_Elmt) loop
+ Subp_Id := Node (Subp_Elmt);
+
+ if Ekind (Subp_Id) = E_Function
+ and then Is_Predicate_Function_M (Subp_Id)
+ then
raise Program_Error;
- else
- S := Subprograms_For_Type (S);
end if;
+
+ Next_Elmt (Subp_Elmt);
end loop;
end Set_Predicate_Function_M;
@@ -8952,8 +9123,8 @@
W ("Has_Independent_Components", Flag34 (Id));
W ("Has_Inheritable_Invariants", Flag248 (Id));
W ("Has_Inherited_Default_Init_Cond", Flag133 (Id));
+ W ("Has_Inherited_Invariants", Flag291 (Id));
W ("Has_Initial_Value", Flag219 (Id));
- W ("Has_Invariants", Flag232 (Id));
W ("Has_Loop_Entry_Attributes", Flag260 (Id));
W ("Has_Machine_Radix_Clause", Flag83 (Id));
W ("Has_Master_Entity", Flag21 (Id));
@@ -8963,6 +9134,7 @@
W ("Has_Non_Standard_Rep", Flag75 (Id));
W ("Has_Out_Or_In_Out_Parameter", Flag110 (Id));
W ("Has_Object_Size_Clause", Flag172 (Id));
+ W ("Has_Own_Invariants", Flag232 (Id));
W ("Has_Per_Object_Constraint", Flag154 (Id));
W ("Has_Pragma_Controlled", Flag27 (Id));
W ("Has_Pragma_Elaborate_Body", Flag150 (Id));
@@ -9086,6 +9258,7 @@
W ("Is_Packed", Flag51 (Id));
W ("Is_Packed_Array_Impl_Type", Flag138 (Id));
W ("Is_Param_Block_Component_Type", Flag215 (Id));
+ W ("Is_Partial_Invariant_Procedure", Flag292 (Id));
W ("Is_Potentially_Use_Visible", Flag9 (Id));
W ("Is_Predicate_Function", Flag255 (Id));
W ("Is_Predicate_Function_M", Flag256 (Id));
===================================================================
@@ -1698,19 +1698,22 @@
-- usual manner.
-- Has_Inheritable_Invariants (Flag248)
+-- Defined in all type entities. Set on private types and interface types
+-- which define at least one class-wide invariant. Such invariants must
+-- be inherited by derived types. The flag is also set on the full view
+-- of a private type for completeness.
-- Has_Inherited_Default_Init_Cond (Flag133) [base type only]
-- Defined in all type entities. Set when a derived type inherits pragma
-- Default_Initial_Condition from its parent type. This flag is mutually
-- exclusive with flag Has_Default_Init_Cond.
+-- Has_Inherited_Invariants (Flag291)
+-- Defined in all type entities. Set on private extensions and derived
+-- types which inherit at least on class-wide invariant from a parent or
+-- an interface type. The flag is also set on the full view of a private
+-- extension for completeness.
+
-- Has_Initial_Value (Flag219)
-- Defined in entities for variables and out parameters. Set if there
-- is an explicit initial value expression in the declaration of the
@@ -1725,15 +1728,10 @@
-- definition contains at least one procedure to which a pragma
-- Interrupt_Handler applies.
+-- Has_Invariants (synthesized)
+-- Defined in all type entities. True if the type defines at least one
+-- invariant of its own or inherits at least one class-wide invariant
+-- from a parent type or an interface.
-- Has_Loop_Entry_Attributes (Flag260)
-- Defined in E_Loop entities. Set when the loop is subject to at least
@@ -1809,6 +1807,11 @@
-- families. Set if they have at least one OUT or IN OUT parameter
-- (allowed for functions only in Ada 2012).
+-- Has_Own_Invariants (Flag232)
+-- Defined in all type entities. Set on any type which defines at least
+-- one invariant of its own. The flag is also set on the full view of a
+-- private extension or a private type for completeness.
+
-- Has_Per_Object_Constraint (Flag154)
-- Defined in E_Component entities. Set if the subtype of the component
-- has a per object constraint. Per object constraints result from the
@@ -2189,15 +2192,18 @@
-- ancestors (Ada 2005: AI-251).
-- Invariant_Procedure (synthesized)
---
+-- Defined in types and subtypes. Set for private types and their full
+-- views if one or more [class-wide] invariants apply to the type, or
+-- when the type inherits class-wide invariants from a parent type or
+-- an interface, or when the type is an array and its component type is
+-- subject to an invariant, or when the type is record and contains a
+-- component subject to an invariant (property is recursive). Points to
+-- to the entity for a procedure which checks all these invariants. The
+-- invariant procedure takes a single argument of the given type, and
+-- returns if the invariant holds, or raises exception Assertion_Error
+-- with an appropriate message if it does not hold. This attribute is
+-- defined but always Empty for private subtypes.
+
-- Note: the reason this is marked as a synthesized attribute is that the
-- way this is stored is as an element of the Subprograms_For_Type field.
@@ -2267,7 +2273,7 @@
-- applies to both the partial view and the full view.
-- Is_Base_Type (synthesized)
+-- Applies to type and subtype entities. True if entity is a base type.
-- Is_Bit_Packed_Array (Flag122) [implementation base type only]
-- Defined in all entities. This flag is set for a packed array type that
@@ -2325,9 +2331,9 @@
-- which are not Completely_Hidden (e.g. discriminants of a root type).
-- Is_Composite_Type (synthesized)
+-- Applies to all entities, true for all composite types and subtypes.
+-- Either Is_Composite_Type or Is_Elementary_Type (but not both) is true
+-- of any type.
-- Is_Concurrent_Record_Type (Flag20)
-- Defined in record types and subtypes. Set if the type was created
@@ -2686,7 +2692,9 @@
-- Is_Invariant_Procedure (Flag257)
-- Defined in functions and procedures. Set for a generated invariant
+-- procedure which verifies the invariants of both the partial and full
+-- views of a private type or private extension as well as any inherited
+-- class-wide invariants from parent types or interfaces.
-- Is_Itype (Flag91)
-- Defined in all entities. Set to indicate that a type is an Itype,
@@ -2912,6 +2920,11 @@
-- component of the parameter block record type generated by the compiler
-- for an entry or a select statement. Read by CodePeer.
+-- Is_Partial_Invariant_Procedure (Flag292)
+-- Defined in functions and procedures. Set for a generated invariant
+-- procedure which verifies the invariants of the partial view of a
+-- private type or private extension.
+
-- Is_Potentially_Use_Visible (Flag9)
-- Defined in all entities. Set if entity is potentially use visible,
-- i.e. it is defined in a package that appears in a currently active
@@ -3738,6 +3751,18 @@
-- of a single protected/task type, the references are examined as they
-- must appear only within the type defintion and the corresponding body.
+-- Partial_Invariant_Procedure (synthesized)
+-- Defined in types and subtypes. Set for private types when one or more
+-- [class-wide] type invariants apply to them. Points to the entity for a
+-- procedure which checks the invariant. This invariant procedure takes a
+-- single argument of the given type, and returns if the invariant holds,
+-- or raises exception Assertion_Error with an appropriate message if it
+-- does not hold. This attribute is defined but always Empty for private
+-- subtypes. This attribute is also set for the corresponding full type.
+--
+-- Note: the reason this is marked as a synthesized attribute is that the
+-- way this is stored is as an element of the Subprograms_For_Type field.
+
-- Partial_View_Has_Unknown_Discr (Flag280)
-- Present in all types. Set to Indicate that the partial view of a type
-- has unknown discriminants. A default initialization of an object of
@@ -4263,15 +4288,14 @@
-- the low bound of the applicable index constraint if there is one,
-- or a copy of the low bound of the index base type if not.
+-- Subprograms_For_Type (Elist29)
+-- Defined in all types. The list may contain the entities of the default
+-- initial condition procedure, invariant procedure, and the two versions
+-- of the predicate function.
+--
+-- Historical note: This attribute used to be a direct linked list of
+-- entities rather than an Elist. The Elist allows greater flexibility
+-- in inheritance of subprograms between views of the same type.
-- Subps_Index (Uint24)
-- Present in subprogram entries. Set if the subprogram contains nested
@@ -5471,7 +5495,7 @@
-- Pending_Access_Types (Elist15)
-- Related_Expression (Node24)
-- Current_Use_Clause (Node27)
- -- Subprograms_For_Type (Node29)
+ -- Subprograms_For_Type (Elist29)
-- Derived_Type_Link (Node31)
-- No_Tagged_Streams_Pragma (Node32)
-- Linker_Section_Pragma (Node33)
@@ -5495,11 +5519,12 @@
-- Has_Discriminants (Flag5)
-- Has_Dynamic_Predicate_Aspect (Flag258)
-- Has_Independent_Components (Flag34) (base type only)
- -- Has_Inheritable_Invariants (Flag248)
+ -- Has_Inheritable_Invariants (Flag248) (base type only)
-- Has_Inherited_Default_Init_Cond (Flag133) (base type only)
- -- Has_Invariants (Flag232)
+ -- Has_Inherited_Invariants (Flag291) (base type only)
-- Has_Non_Standard_Rep (Flag75) (base type only)
-- Has_Object_Size_Clause (Flag172)
+ -- Has_Own_Invariants (Flag232) (base type only)
-- Has_Pragma_Preelab_Init (Flag221)
-- Has_Pragma_Unreferenced_Objects (Flag212)
-- Has_Predicates (Flag250)
@@ -5553,11 +5578,13 @@
-- Alignment_Clause (synth)
-- Base_Type (synth)
-- Default_Init_Cond_Procedure (synth)
+ -- Has_Invariants (synth)
-- Implementation_Base_Type (synth)
-- Invariant_Procedure (synth)
-- Is_Access_Protected_Subprogram_Type (synth)
-- Is_Atomic_Or_VFA (synth)
-- Is_Controlled_Active (synth)
+ -- Partial_Invariant_Procedure (synth)
-- Predicate_Function (synth)
-- Predicate_Function_M (synth)
-- Root_Type (synth)
@@ -5921,7 +5948,6 @@
-- Overridden_Operation (Node26)
-- Wrapped_Entity (Node27) (non-generic case only)
-- Extra_Formals (Node28)
- -- Subprograms_For_Type (Node29)
-- Corresponding_Equality (Node30) (implicit /= only)
-- Thunk_Entity (Node31) (thunk case only)
-- Corresponding_Procedure (Node32) (generate C code only)
@@ -5942,7 +5968,6 @@
-- Has_Completion (Flag26)
-- Has_Controlling_Result (Flag98)
-- Has_Expanded_Contract (Flag240) (non-generic case only)
- -- Has_Invariants (Flag232)
-- Has_Master_Entity (Flag21)
-- Has_Missing_Return (Flag142)
-- Has_Nested_Block_With_Handler (Flag101)
@@ -5952,6 +5977,7 @@
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Called (Flag102) (non-generic case only)
-- Is_Constructor (Flag76)
+ -- Is_Default_Init_Cond_Procedure (Flag132) (non-generic case only)
-- Is_Discrim_SO_Function (Flag176)
-- Is_Discriminant_Check_Function (Flag264)
-- Is_Eliminated (Flag124)
@@ -5962,6 +5988,7 @@
-- Is_Intrinsic_Subprogram (Flag64)
-- Is_Invariant_Procedure (Flag257) (non-generic case only)
-- Is_Machine_Code_Subprogram (Flag137) (non-generic case only)
+ -- Is_Partial_Invariant_Procedure (Flag292) (non-generic case only)
-- Is_Predicate_Function (Flag255) (non-generic case only)
-- Is_Predicate_Function_M (Flag256) (non-generic case only)
-- Is_Primitive (Flag218)
@@ -6094,13 +6121,11 @@
-- Last_Entity (Node20)
-- Subps_Index (Uint24)
-- Overridden_Operation (Node26)
- -- Subprograms_For_Type (Node29)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35)
-- SPARK_Pragma (Node40)
-- Default_Expressions_Processed (Flag108)
- -- Has_Invariants (Flag232)
-- Has_Nested_Subprogram (Flag282)
-- Is_Intrinsic_Subprogram (Flag64)
-- Is_Machine_Code_Subprogram (Flag137)
@@ -6254,7 +6279,6 @@
-- Discard_Names (Flag88)
-- Has_Completion (Flag26)
-- Has_Expanded_Contract (Flag240) (non-generic case only)
- -- Has_Invariants (Flag232)
-- Has_Master_Entity (Flag21)
-- Has_Nested_Block_With_Handler (Flag101)
-- Has_Nested_Subprogram (Flag282)
@@ -6273,6 +6297,7 @@
-- Is_Invariant_Procedure (Flag257) (non-generic case only)
-- Is_Machine_Code_Subprogram (Flag137) (non-generic case only)
-- Is_Null_Init_Proc (Flag178)
+ -- Is_Partial_Invariant_Procedure (Flag292) (non-generic case only)
-- Is_Predicate_Function (Flag255) (non-generic case only)
-- Is_Predicate_Function_M (Flag256) (non-generic case only)
-- Is_Primitive (Flag218)
@@ -6918,6 +6943,7 @@
function Has_Independent_Components (Id : E) return B;
function Has_Inheritable_Invariants (Id : E) return B;
function Has_Inherited_Default_Init_Cond (Id : E) return B;
+ function Has_Inherited_Invariants (Id : E) return B;
function Has_Initial_Value (Id : E) return B;
function Has_Interrupt_Handler (Id : E) return B;
function Has_Invariants (Id : E) return B;
@@ -6930,6 +6956,7 @@
function Has_Non_Standard_Rep (Id : E) return B;
function Has_Object_Size_Clause (Id : E) return B;
function Has_Out_Or_In_Out_Parameter (Id : E) return B;
+ function Has_Own_Invariants (Id : E) return B;
function Has_Per_Object_Constraint (Id : E) return B;
function Has_Pragma_Controlled (Id : E) return B;
function Has_Pragma_Elaborate_Body (Id : E) return B;
@@ -7058,6 +7085,7 @@
function Is_Packed_Array_Impl_Type (Id : E) return B;
function Is_Potentially_Use_Visible (Id : E) return B;
function Is_Param_Block_Component_Type (Id : E) return B;
+ function Is_Partial_Invariant_Procedure (Id : E) return B;
function Is_Predicate_Function (Id : E) return B;
function Is_Predicate_Function_M (Id : E) return B;
function Is_Preelaborated (Id : E) return B;
@@ -7208,7 +7236,7 @@
function Strict_Alignment (Id : E) return B;
function String_Literal_Length (Id : E) return U;
function String_Literal_Low_Bound (Id : E) return N;
- function Subprograms_For_Type (Id : E) return E;
+ function Subprograms_For_Type (Id : E) return L;
function Subps_Index (Id : E) return U;
function Suppress_Elaboration_Warnings (Id : E) return B;
function Suppress_Initialization (Id : E) return B;
@@ -7589,8 +7617,8 @@
procedure Set_Has_Independent_Components (Id : E; V : B := True);
procedure Set_Has_Inheritable_Invariants (Id : E; V : B := True);
procedure Set_Has_Inherited_Default_Init_Cond (Id : E; V : B := True);
+ procedure Set_Has_Inherited_Invariants (Id : E; V : B := True);
procedure Set_Has_Initial_Value (Id : E; V : B := True);
- procedure Set_Has_Invariants (Id : E; V : B := True);
procedure Set_Has_Loop_Entry_Attributes (Id : E; V : B := True);
procedure Set_Has_Machine_Radix_Clause (Id : E; V : B := True);
procedure Set_Has_Master_Entity (Id : E; V : B := True);
@@ -7600,6 +7628,7 @@
procedure Set_Has_Non_Standard_Rep (Id : E; V : B := True);
procedure Set_Has_Object_Size_Clause (Id : E; V : B := True);
procedure Set_Has_Out_Or_In_Out_Parameter (Id : E; V : B := True);
+ procedure Set_Has_Own_Invariants (Id : E; V : B := True);
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True);
procedure Set_Has_Pragma_Controlled (Id : E; V : B := True);
procedure Set_Has_Pragma_Elaborate_Body (Id : E; V : B := True);
@@ -7732,6 +7761,7 @@
procedure Set_Is_Packed (Id : E; V : B := True);
procedure Set_Is_Packed_Array_Impl_Type (Id : E; V : B := True);
procedure Set_Is_Param_Block_Component_Type (Id : E; V : B := True);
+ procedure Set_Is_Partial_Invariant_Procedure (Id : E; V : B := True);
procedure Set_Is_Potentially_Use_Visible (Id : E; V : B := True);
procedure Set_Is_Predicate_Function (Id : E; V : B := True);
procedure Set_Is_Predicate_Function_M (Id : E; V : B := True);
@@ -7882,7 +7912,7 @@
procedure Set_Strict_Alignment (Id : E; V : B := True);
procedure Set_String_Literal_Length (Id : E; V : U);
procedure Set_String_Literal_Low_Bound (Id : E; V : N);
- procedure Set_Subprograms_For_Type (Id : E; V : E);
+ procedure Set_Subprograms_For_Type (Id : E; V : L);
procedure Set_Subps_Index (Id : E; V : U);
procedure Set_Suppress_Elaboration_Warnings (Id : E; V : B := True);
procedure Set_Suppress_Initialization (Id : E; V : B := True);
@@ -7911,11 +7941,13 @@
function Default_Init_Cond_Procedure (Id : E) return E;
function Invariant_Procedure (Id : E) return E;
+ function Partial_Invariant_Procedure (Id : E) return E;
function Predicate_Function (Id : E) return E;
function Predicate_Function_M (Id : E) return E;
procedure Set_Default_Init_Cond_Procedure (Id : E; V : E);
procedure Set_Invariant_Procedure (Id : E; V : E);
+ procedure Set_Partial_Invariant_Procedure (Id : E; V : E);
procedure Set_Predicate_Function (Id : E; V : E);
procedure Set_Predicate_Function_M (Id : E; V : E);
@@ -8374,8 +8406,8 @@
pragma Inline (Has_Independent_Components);
pragma Inline (Has_Inheritable_Invariants);
pragma Inline (Has_Inherited_Default_Init_Cond);
+ pragma Inline (Has_Inherited_Invariants);
pragma Inline (Has_Initial_Value);
- pragma Inline (Has_Invariants);
pragma Inline (Has_Loop_Entry_Attributes);
pragma Inline (Has_Machine_Radix_Clause);
pragma Inline (Has_Master_Entity);
@@ -8385,6 +8417,7 @@
pragma Inline (Has_Non_Standard_Rep);
pragma Inline (Has_Object_Size_Clause);
pragma Inline (Has_Out_Or_In_Out_Parameter);
+ pragma Inline (Has_Own_Invariants);
pragma Inline (Has_Per_Object_Constraint);
pragma Inline (Has_Pragma_Controlled);
pragma Inline (Has_Pragma_Elaborate_Body);
@@ -8550,6 +8583,7 @@
pragma Inline (Is_Packed);
pragma Inline (Is_Packed_Array_Impl_Type);
pragma Inline (Is_Param_Block_Component_Type);
+ pragma Inline (Is_Partial_Invariant_Procedure);
pragma Inline (Is_Potentially_Use_Visible);
pragma Inline (Is_Predicate_Function);
pragma Inline (Is_Predicate_Function_M);
@@ -8884,8 +8918,8 @@
pragma Inline (Set_Has_Independent_Components);
pragma Inline (Set_Has_Inheritable_Invariants);
pragma Inline (Set_Has_Inherited_Default_Init_Cond);
+ pragma Inline (Set_Has_Inherited_Invariants);
pragma Inline (Set_Has_Initial_Value);
- pragma Inline (Set_Has_Invariants);
pragma Inline (Set_Has_Loop_Entry_Attributes);
pragma Inline (Set_Has_Machine_Radix_Clause);
pragma Inline (Set_Has_Master_Entity);
@@ -8895,6 +8929,7 @@
pragma Inline (Set_Has_Non_Standard_Rep);
pragma Inline (Set_Has_Object_Size_Clause);
pragma Inline (Set_Has_Out_Or_In_Out_Parameter);
+ pragma Inline (Set_Has_Own_Invariants);
pragma Inline (Set_Has_Per_Object_Constraint);
pragma Inline (Set_Has_Pragma_Controlled);
pragma Inline (Set_Has_Pragma_Elaborate_Body);
@@ -9026,6 +9061,7 @@
pragma Inline (Set_Is_Packed);
pragma Inline (Set_Is_Packed_Array_Impl_Type);
pragma Inline (Set_Is_Param_Block_Component_Type);
+ pragma Inline (Set_Is_Partial_Invariant_Procedure);
pragma Inline (Set_Is_Potentially_Use_Visible);
pragma Inline (Set_Is_Predicate_Function);
pragma Inline (Set_Is_Predicate_Function_M);
===================================================================
@@ -39,6 +39,7 @@
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
+with Exp_Ch7; use Exp_Ch7;
with Exp_Dist; use Exp_Dist;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
@@ -16503,8 +16504,20 @@
when Pragma_Invariant => Invariant : declare
Discard : Boolean;
Typ : Entity_Id;
- Type_Id : Node_Id;
+ Typ_Arg : Node_Id;
+ CRec_Typ : Entity_Id;
+ -- The corresponding record type of Full_Typ
+
+ Full_Base : Entity_Id;
+ -- The base type of Full_Typ
+
+ Full_Typ : Entity_Id;
+ -- The full view of Typ
+
+ Priv_Typ : Entity_Id;
+ -- The partial view of Typ
+
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
@@ -16519,14 +16532,16 @@
Check_Arg_Is_Local_Name (Arg1);
- Type_Id := Get_Pragma_Arg (Arg1);
- Find_Type (Type_Id);
- Typ := Entity (Type_Id);
+ Typ_Arg := Get_Pragma_Arg (Arg1);
+ Find_Type (Typ_Arg);
+ Typ := Entity (Typ_Arg);
+ -- Nothing to do of the related type is erroneous in some way
+
if Typ = Any_Type then
return;
- -- Invariants allowed in interface types (RM 7.3.2(3/3))
+ -- AI12-0041: Invariants are allowed in interface types
elsif Is_Interface (Typ) then
null;
@@ -16536,64 +16551,86 @@
-- a class-wide invariant can only appear on a private declaration
-- or private extension, not a completion.
- elsif Ekind_In (Typ, E_Private_Type,
- E_Record_Type_With_Private,
- E_Limited_Private_Type)
+ -- A [class-wide] invariant may be associated a [limited] private
+ -- type or a private extension.
+
+ elsif Ekind_In (Typ, E_Limited_Private_Type,
+ E_Private_Type,
+ E_Record_Type_With_Private)
then
null;
- elsif In_Private_Part (Current_Scope)
- and then Has_Private_Declaration (Typ)
+ -- A non-class-wide invariant may be associated with the full view
+ -- of a [limited] private type or a private extension.
+
+ elsif Has_Private_Declaration (Typ)
and then not Class_Present (N)
then
null;
- elsif In_Private_Part (Current_Scope) then
+ -- A class-wide invariant may appear on the partial view only
+
+ elsif Class_Present (N) then
Error_Pragma_Arg
- ("pragma% only allowed for private type declared in "
- & "visible part", Arg1);
+ ("pragma % only allowed for private type", Arg1);
+ return;
+ -- A regular invariant may appear on both views
+
else
Error_Pragma_Arg
- ("pragma% only allowed for private type", Arg1);
+ ("pragma % only allowed for private type or corresponding "
+ & "full view", Arg1);
+ return;
end if;
+ -- An invariant associated with an abstract type (this includes
+ -- interfaces) must be class-wide.
+
+ if Is_Abstract_Type (Typ) and then not Class_Present (N) then
+ Error_Pragma_Arg
+ ("pragma % not allowed for abstract type", Arg1);
+ return;
+ end if;
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
Mark_Pragma_As_Ghost (N, Typ);
- -- Not allowed for abstract type in the non-class case (it is
- -- allowed to use Invariant'Class for abstract types).
+ -- The pragma defines a type-specific invariant, the type is said
+ -- to have invariants of its "own".
- if Is_Abstract_Type (Typ) and then not Class_Present (N) then
- Error_Pragma_Arg
- ("pragma% not allowed for abstract type", Arg1);
+ Set_Has_Own_Invariants (Typ);
+
+ -- If the invariant is class-wide, then it can be inherited by
+ -- derived or interface implementing types. The type is said to
+ -- have "inheritable" invariants.
+
+ if Class_Present (N) then
+ Set_Has_Inheritable_Invariants (Typ);
end if;
- -- Link the pragma on to the rep item chain, for processing when
+ Get_Views (Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
+
+ -- Propagate invariant-related attributes to all views of the type
+ -- and any additional types that may have been created.
+
+ Propagate_Invariant_Attributes (Priv_Typ, From_Typ => Typ);
+ Propagate_Invariant_Attributes (Full_Typ, From_Typ => Typ);
+ Propagate_Invariant_Attributes (Full_Base, From_Typ => Typ);
+ Propagate_Invariant_Attributes (CRec_Typ, From_Typ => Typ);
+
+ -- Chain the pragma on to the rep item chain, for processing when
-- the type is frozen.
Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
- -- Note that the type has at least one invariant, and also that
- -- it has inheritable invariants if we have Invariant'Class
- -- or Type_Invariant'Class. Build the corresponding invariant
- -- procedure declaration, so that calls to it can be generated
- -- before the body is built (e.g. within an expression function).
+ -- Create the declaration of the invariant procedure which will
+ -- verify the invariant at run-time. Note that interfaces do not
+ -- carry such a declaration.
- -- Interface types have no invariant procedure; their invariants
- -- are propagated to the build invariant procedure of all the
- -- types covering the interface type.
-
- if not Is_Interface (Typ) then
- Insert_After_And_Analyze
- (N, Build_Invariant_Procedure_Declaration (Typ));
- end if;
-
- if Class_Present (N) then
- Set_Has_Inheritable_Invariants (Typ);
- end if;
+ Build_Invariant_Procedure_Declaration (Typ);
end Invariant;
----------------
===================================================================
@@ -2290,6 +2290,25 @@
Set_Has_Unchecked_Union (Arr);
end if;
+ -- The array type requires its own invariant procedure in order to
+ -- verify the component invariant over all elements.
+
+ if Has_Invariants (Component_Type (Arr))
+ or else
+ (Is_Access_Type (Component_Type (Arr))
+ and then Has_Invariants
+ (Designated_Type (Component_Type (Arr))))
+ then
+ Set_Has_Own_Invariants (Arr);
+
+ -- The array type is an implementation base type. Propagate the
+ -- same property to the first subtype.
+
+ if Is_Itype (Arr) then
+ Set_Has_Own_Invariants (First_Subtype (Arr));
+ end if;
+ end if;
+
-- Warn for pragma Pack overriding foreign convention
if Has_Foreign_Convention (Ctyp)
@@ -4165,7 +4184,8 @@
Freeze_And_Append (Corresponding_Remote_Type (Rec), N, Result);
end if;
- -- Check for controlled components and unchecked unions.
+ -- Check for controlled components, unchecked unions, and type
+ -- invariants.
Comp := First_Component (Rec);
while Present (Comp) loop
@@ -4194,6 +4214,22 @@
Set_Has_Unchecked_Union (Rec);
end if;
+ -- The record type requires its own invariant procedure in
+ -- order to verify the invariant of each individual component.
+ -- Do not consider internal components such as _parent because
+ -- parent class-wide invariants are always inherited.
+
+ if Comes_From_Source (Comp)
+ and then
+ (Has_Invariants (Etype (Comp))
+ or else
+ (Is_Access_Type (Etype (Comp))
+ and then Has_Invariants
+ (Designated_Type (Etype (Comp)))))
+ then
+ Set_Has_Own_Invariants (Rec);
+ end if;
+
-- Scan component declaration for likely misuses of current
-- instance, either in a constraint or a default expression.
@@ -5224,8 +5260,7 @@
and then not Is_Tagged_Type (E)
then
Error_Msg_NE
- ("Type_Invariant''Class cannot be specified for &",
- Prag, E);
+ ("Type_Invariant''Class cannot be specified for &", Prag, E);
Error_Msg_N
("\can only be specified for a tagged type", Prag);
end if;
===================================================================
@@ -8622,6 +8622,76 @@
return Empty;
end Get_User_Defined_Eq;
+ ---------------
+ -- Get_Views --
+ ---------------
+
+ procedure Get_Views
+ (Typ : Entity_Id;
+ Priv_Typ : out Entity_Id;
+ Full_Typ : out Entity_Id;
+ Full_Base : out Entity_Id;
+ CRec_Typ : out Entity_Id)
+ is
+ begin
+ -- Assume that none of the views can be recovered
+
+ Priv_Typ := Empty;
+ Full_Typ := Empty;
+ Full_Base := Empty;
+ CRec_Typ := Empty;
+
+ -- The input type is private
+
+ if Is_Private_Type (Typ) then
+ Priv_Typ := Typ;
+ Full_Typ := Full_View (Priv_Typ);
+
+ if Present (Full_Typ) then
+ Full_Base := Base_Type (Full_Typ);
+
+ if Ekind_In (Full_Typ, E_Protected_Type, E_Task_Type) then
+ CRec_Typ := Corresponding_Record_Type (Full_Typ);
+ end if;
+ end if;
+
+ -- The input type is the corresponding record type of a protected or a
+ -- task type.
+
+ elsif Ekind (Typ) = E_Record_Type
+ and then Is_Concurrent_Record_Type (Typ)
+ then
+ CRec_Typ := Typ;
+ Full_Typ := Corresponding_Concurrent_Type (CRec_Typ);
+ Full_Base := Base_Type (Full_Typ);
+ Priv_Typ := Incomplete_Or_Partial_View (Full_Typ);
+
+ -- Otherwise the input type could be the full view of a private type
+
+ else
+ Full_Typ := Typ;
+ Full_Base := Base_Type (Full_Typ);
+
+ if Ekind_In (Full_Typ, E_Protected_Type, E_Task_Type) then
+ CRec_Typ := Corresponding_Record_Type (Full_Typ);
+ end if;
+
+ -- The type is the full view of a private type, obtain the partial
+ -- view.
+
+ if Has_Private_Declaration (Full_Typ)
+ and then not Is_Private_Type (Full_Typ)
+ then
+ Priv_Typ := Incomplete_Or_Partial_View (Full_Typ);
+
+ -- The full view of a private type should always have a partial
+ -- view.
+
+ pragma Assert (Present (Priv_Typ));
+ end if;
+ end if;
+ end Get_Views;
+
-----------------------
-- Has_Access_Values --
-----------------------
@@ -10988,20 +11058,31 @@
while Present (Decl) loop
Match := Empty;
+ -- The partial view of a Taft-amendment type is an incomplete
+ -- type.
+
if Taft then
if Nkind (Decl) = N_Incomplete_Type_Declaration then
Match := Defining_Identifier (Decl);
end if;
- else
- if Nkind_In (Decl, N_Private_Extension_Declaration,
+ -- Otherwise look for a private type whose full view matches the
+ -- input type. Note that this checks full_type_declaration nodes
+ -- to account for derivations from a private type where the type
+ -- declaration hold the partial view and the full view is an
+ -- itype.
+
+ elsif Nkind_In (Decl, N_Full_Type_Declaration,
+ N_Private_Extension_Declaration,
N_Private_Type_Declaration)
- then
- Match := Defining_Identifier (Decl);
- end if;
+ then
+ Match := Defining_Identifier (Decl);
end if;
+ -- Guard against unanalyzed entities
+
if Present (Match)
+ and then Is_Type (Match)
and then Present (Full_View (Match))
and then Full_View (Match) = Id
then
@@ -11040,7 +11121,9 @@
Pkg_Decl : Node_Id := Pkg;
begin
- if Present (Pkg) and then Ekind (Pkg) = E_Package then
+ if Present (Pkg)
+ and then Ekind_In (Pkg, E_Generic_Package, E_Package)
+ then
while Nkind (Pkg_Decl) /= N_Package_Specification loop
Pkg_Decl := Parent (Pkg_Decl);
end loop;
@@ -18519,13 +18602,71 @@
Set_Sloc (Endl, Loc);
end Process_End_Label;
+ ------------------------------------
+ -- Propagate_Invariant_Attributes --
+ ------------------------------------
+
+ procedure Propagate_Invariant_Attributes
+ (Typ : Entity_Id;
+ From_Typ : Entity_Id)
+ is
+ Full_IP : Entity_Id;
+ Part_IP : Entity_Id;
+
+ begin
+ if Present (Typ) and then Present (From_Typ) then
+ pragma Assert (Is_Type (Typ) and then Is_Type (From_Typ));
+
+ -- Nothing to do if both the source and the destination denote the
+ -- same type.
+
+ if From_Typ = Typ then
+ return;
+ end if;
+
+ Full_IP := Invariant_Procedure (From_Typ);
+ Part_IP := Partial_Invariant_Procedure (From_Typ);
+
+ -- The setting of the attributes is intentionally conservative. This
+ -- prevents accidental clobbering of enabled attributes.
+
+ if Has_Inheritable_Invariants (From_Typ)
+ and then not Has_Inheritable_Invariants (Typ)
+ then
+ Set_Has_Inheritable_Invariants (Typ, True);
+ end if;
+
+ if Has_Inherited_Invariants (From_Typ)
+ and then not Has_Inherited_Invariants (Typ)
+ then
+ Set_Has_Inherited_Invariants (Typ, True);
+ end if;
+
+ if Has_Own_Invariants (From_Typ)
+ and then not Has_Own_Invariants (Typ)
+ then
+ Set_Has_Own_Invariants (Typ, True);
+ end if;
+
+ if Present (Full_IP) and then No (Invariant_Procedure (Typ)) then
+ Set_Invariant_Procedure (Typ, Full_IP);
+ end if;
+
+ if Present (Part_IP) and then No (Partial_Invariant_Procedure (Typ))
+ then
+ Set_Partial_Invariant_Procedure (Typ, Part_IP);
+ end if;
+ end if;
+ end Propagate_Invariant_Attributes;
+
--------------------------------
-- Propagate_Concurrent_Flags --
--------------------------------
procedure Propagate_Concurrent_Flags
(Typ : Entity_Id;
- Comp_Typ : Entity_Id) is
+ Comp_Typ : Entity_Id)
+ is
begin
if Has_Task (Comp_Typ) then
Set_Has_Task (Typ);
===================================================================
@@ -1005,6 +1005,20 @@
-- For a type entity, return the entity of the primitive equality function
-- for the type if it exists, otherwise return Empty.
+ procedure Get_Views
+ (Typ : Entity_Id;
+ Priv_Typ : out Entity_Id;
+ Full_Typ : out Entity_Id;
+ Full_Base : out Entity_Id;
+ CRec_Typ : out Entity_Id);
+ -- Obtain the partial and full view of type Typ and in addition any extra
+ -- types the full view may have. The return entities are as follows:
+ --
+ -- Priv_Typ - the partial view (a private type)
+ -- Full_Typ - the full view
+ -- Full_Base - the base type of the full view
+ -- CRec_Typ - the corresponding record type of the full view
+
function Has_Access_Values (T : Entity_Id) return Boolean;
-- Returns true if type or subtype T is an access type, or has a component
-- (at any recursive level) that is an access type. This is a conservative
@@ -2022,6 +2036,12 @@
-- parameter Ent gives the entity to which the End_Label refers,
-- and to which cross-references are to be generated.
+ procedure Propagate_Invariant_Attributes
+ (Typ : Entity_Id;
+ From_Typ : Entity_Id);
+ -- Inherit all invariant-related attributes form type From_Typ. Typ is the
+ -- destination type.
+
procedure Propagate_Concurrent_Flags
(Typ : Entity_Id;
Comp_Typ : Entity_Id);
===================================================================
@@ -4223,14 +4223,19 @@
then
Error_Msg_NE ("actual for& must be a variable", A, F);
- if Is_Subprogram (Current_Scope)
- and then
- (Is_Invariant_Procedure (Current_Scope)
- or else Is_Predicate_Function (Current_Scope))
- then
- Error_Msg_N
- ("function used in predicate cannot "
- & "modify its argument", F);
+ if Is_Subprogram (Current_Scope) then
+ if Is_Invariant_Procedure (Current_Scope)
+ or else Is_Partial_Invariant_Procedure (Current_Scope)
+ then
+ Error_Msg_N
+ ("function used in invariant cannot modify its "
+ & "argument", F);
+
+ elsif Is_Predicate_Function (Current_Scope) then
+ Error_Msg_N
+ ("function used in predicate cannot modify its "
+ & "argument", F);
+ end if;
end if;
end if;
===================================================================
@@ -4428,6 +4428,34 @@
-- both subprogram bodies and subprogram declarations (specs).
function Analyze_Subprogram_Specification (N : Node_Id) return Entity_Id is
+ function Is_Invariant_Procedure_Or_Body (E : Entity_Id) return Boolean;
+ -- Determine whether entity E denotes the spec or body of an invariant
+ -- procedure.
+
+ ------------------------------------
+ -- Is_Invariant_Procedure_Or_Body --
+ ------------------------------------
+
+ function Is_Invariant_Procedure_Or_Body (E : Entity_Id) return Boolean is
+ Decl : constant Node_Id := Unit_Declaration_Node (E);
+ Spec : Entity_Id;
+
+ begin
+ if Nkind (Decl) = N_Subprogram_Body then
+ Spec := Corresponding_Spec (Decl);
+ else
+ Spec := E;
+ end if;
+
+ return
+ Present (Spec)
+ and then Ekind (Spec) = E_Procedure
+ and then (Is_Partial_Invariant_Procedure (Spec)
+ or else Is_Invariant_Procedure (Spec));
+ end Is_Invariant_Procedure_Or_Body;
+
+ -- Local variables
+
Designator : constant Entity_Id := Defining_Entity (N);
Formals : constant List_Id := Parameter_Specifications (N);
@@ -4487,7 +4515,27 @@
-- Same processing for an access parameter whose designated type is
-- derived from a synchronized interface.
- if Ada_Version >= Ada_2005 then
+ -- This modification is not done for invariant procedures because
+ -- the corresponding record may not necessarely be visible when the
+ -- concurrent type acts as the full view of a private type.
+
+ -- package Pack is
+ -- type Prot is private with Type_Invariant => ...;
+ -- procedure ConcInvariant (Obj : Prot);
+ -- private
+ -- protected type Prot is ...;
+ -- type Concurrent_Record_Prot is record ...;
+ -- procedure ConcInvariant (Obj : Prot) is
+ -- ...
+ -- end ConcInvariant;
+ -- end Pack;
+
+ -- In the example above, both the spec and body of the invariant
+ -- procedure must utilize the private type as the controlling type.
+
+ if Ada_Version >= Ada_2005
+ and then not Is_Invariant_Procedure_Or_Body (Designator)
+ then
declare
Formal : Entity_Id;
Formal_Typ : Entity_Id;
===================================================================
@@ -3317,6 +3317,17 @@
end if;
end Elist26;
+ function Elist29 (N : Node_Id) return Elist_Id is
+ pragma Assert (Nkind (N) in N_Entity);
+ Value : constant Union_Id := Nodes.Table (N + 4).Field11;
+ begin
+ if Value = 0 then
+ return No_Elist;
+ else
+ return Elist_Id (Value);
+ end if;
+ end Elist29;
+
function Elist36 (N : Node_Id) return Elist_Id is
pragma Assert (Nkind (N) in N_Entity);
Value : constant Union_Id := Nodes.Table (N + 6).Field6;
@@ -6109,6 +6120,12 @@
Nodes.Table (N + 4).Field8 := Union_Id (Val);
end Set_Elist26;
+ procedure Set_Elist29 (N : Node_Id; Val : Elist_Id) is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ Nodes.Table (N + 4).Field11 := Union_Id (Val);
+ end Set_Elist29;
+
procedure Set_Elist36 (N : Node_Id; Val : Elist_Id) is
begin
pragma Assert (Nkind (N) in N_Entity);
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -1473,6 +1473,9 @@
function Elist26 (N : Node_Id) return Elist_Id;
pragma Inline (Elist26);
+ function Elist29 (N : Node_Id) return Elist_Id;
+ pragma Inline (Elist29);
+
function Elist36 (N : Node_Id) return Elist_Id;
pragma Inline (Elist36);
@@ -2836,6 +2839,9 @@
procedure Set_Elist26 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist26);
+ procedure Set_Elist29 (N : Node_Id; Val : Elist_Id);
+ pragma Inline (Set_Elist29);
+
procedure Set_Elist36 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist36);
===================================================================
@@ -62,7 +62,6 @@
with Snames; use Snames;
with Stand; use Stand;
with Sinfo; use Sinfo;
-with Stringt; use Stringt;
with Targparm; use Targparm;
with Ttypes; use Ttypes;
with Tbuild; use Tbuild;
@@ -8080,577 +8079,7 @@
return Prag;
end Build_Export_Import_Pragma;
- -------------------------------------------
- -- Build_Invariant_Procedure_Declaration --
- -------------------------------------------
-
- function Build_Invariant_Procedure_Declaration
- (Typ : Entity_Id) return Node_Id
- is
- Loc : constant Source_Ptr := Sloc (Typ);
- Decl : Node_Id;
- Obj_Id : Entity_Id;
- SId : Entity_Id;
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
- begin
- -- Check for duplicate definitions
-
- if Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)) then
- return Empty;
- end if;
-
- -- The related type may be subject to pragma Ghost. Set the mode now to
- -- ensure that the invariant procedure is properly marked as Ghost.
-
- Set_Ghost_Mode_From_Entity (Typ);
-
- SId :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Typ), "Invariant"));
- Set_Has_Invariants (Typ);
- Set_Ekind (SId, E_Procedure);
- Set_Etype (SId, Standard_Void_Type);
- Set_Is_Invariant_Procedure (SId);
- Set_Invariant_Procedure (Typ, SId);
-
- -- Source Coverage Obligations might be attached to the invariant
- -- expression this procedure evaluates, and we need debug info to be
- -- able to assess the coverage achieved by evaluations.
-
- if Opt.Generate_SCO then
- Set_Needs_Debug_Info (SId);
- end if;
-
- -- Mark the invariant procedure explicitly as Ghost because it does not
- -- come from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (SId);
- end if;
-
- Obj_Id := Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
- Set_Etype (Obj_Id, Typ);
-
- Decl :=
- Make_Subprogram_Declaration (Loc,
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => SId,
- Parameter_Specifications => New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Obj_Id,
- Parameter_Type => New_Occurrence_Of (Typ, Loc)))));
-
- Ghost_Mode := Save_Ghost_Mode;
-
- return Decl;
- end Build_Invariant_Procedure_Declaration;
-
-------------------------------
- -- Build_Invariant_Procedure --
- -------------------------------
-
- -- The procedure that is constructed here has the form
-
- -- procedure typInvariant (Ixxx : typ) is
- -- begin
- -- pragma Check (Invariant, exp, "failed invariant from xxx");
- -- pragma Check (Invariant, exp, "failed invariant from xxx");
- -- ...
- -- pragma Check (Invariant, exp, "failed inherited invariant from xxx");
- -- ...
- -- end typInvariant;
-
- procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id) is
- procedure Add_Invariants
- (T : Entity_Id;
- Obj_Id : Entity_Id;
- Stmts : in out List_Id;
- Inherit : Boolean);
- -- Appends statements to Stmts for any invariants in the rep item chain
- -- of the given type. If Inherit is False, then we only process entries
- -- on the chain for the type Typ. If Inherit is True, then we ignore any
- -- Invariant aspects, but we process all Invariant'Class aspects, adding
- -- "inherited" to the exception message and generating an informational
- -- message about the inheritance of an invariant.
-
- --------------------
- -- Add_Invariants --
- --------------------
-
- procedure Add_Invariants
- (T : Entity_Id;
- Obj_Id : Entity_Id;
- Stmts : in out List_Id;
- Inherit : Boolean)
- is
- procedure Add_Invariant (Prag : Node_Id);
- -- Create a runtime check to verify the exression of invariant pragma
- -- Prag. All generated code is added to list Stmts.
-
- -------------------
- -- Add_Invariant --
- -------------------
-
- procedure Add_Invariant (Prag : Node_Id) is
- procedure Replace_Type_Reference (N : Node_Id);
- -- Replace a single occurrence N of the subtype name with a
- -- reference to the formal of the predicate function. N can be an
- -- identifier referencing the subtype, or a selected component,
- -- representing an appropriately qualified occurrence of the
- -- subtype name.
-
- procedure Replace_Type_References is
- new Replace_Type_References_Generic (Replace_Type_Reference);
- -- Traverse an expression replacing all occurrences of the subtype
- -- name with appropriate references to the formal of the predicate
- -- function. Note that we must ensure that the type and entity
- -- information is properly set in the replacement node, since we
- -- will do a Preanalyze call of this expression without proper
- -- visibility of the procedure argument.
-
- ----------------------------
- -- Replace_Type_Reference --
- ----------------------------
-
- -- Note: See comments in Add_Predicates.Replace_Type_Reference
- -- regarding handling of Sloc and Comes_From_Source.
-
- procedure Replace_Type_Reference (N : Node_Id) is
- Nloc : constant Source_Ptr := Sloc (N);
-
- begin
- -- Add semantic information to node to be rewritten, for ASIS
- -- navigation needs.
-
- if Nkind (N) = N_Identifier then
- Set_Entity (N, T);
- Set_Etype (N, T);
-
- elsif Nkind (N) = N_Selected_Component then
- Analyze (Prefix (N));
- Set_Entity (Selector_Name (N), T);
- Set_Etype (Selector_Name (N), T);
- end if;
-
- -- Invariant'Class, replace with T'Class (obj)
-
- if Class_Present (Prag) then
-
- -- In ASIS mode, an inherited item is already analyzed,
- -- and the replacement has been done, so do not repeat
- -- the transformation to prevent a malformed tree.
-
- if ASIS_Mode
- and then Nkind (Parent (N)) = N_Attribute_Reference
- and then Attribute_Name (Parent (N)) = Name_Class
- then
- null;
-
- else
- Rewrite (N,
- Make_Type_Conversion (Nloc,
- Subtype_Mark =>
- Make_Attribute_Reference (Nloc,
- Prefix => New_Occurrence_Of (T, Nloc),
- Attribute_Name => Name_Class),
- Expression =>
- Make_Identifier (Nloc, Chars (Obj_Id))));
-
- Set_Entity (Expression (N), Obj_Id);
- Set_Etype (Expression (N), Typ);
- end if;
-
- -- Invariant, replace with obj
-
- else
- Rewrite (N, Make_Identifier (Nloc, Chars (Obj_Id)));
- Set_Entity (N, Obj_Id);
- Set_Etype (N, Typ);
- end if;
-
- Set_Comes_From_Source (N, True);
- end Replace_Type_Reference;
-
- -- Local variables
-
- Asp : constant Node_Id := Corresponding_Aspect (Prag);
- Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
- Ploc : constant Source_Ptr := Sloc (Prag);
- Arg1 : Node_Id;
- Arg2 : Node_Id;
- Arg3 : Node_Id;
- Assoc : List_Id;
- Expr : Node_Id;
- Str : String_Id;
-
- -- Start of processing for Add_Invariant
-
- begin
- -- Extract the arguments of the invariant pragma
-
- Arg1 := First (Pragma_Argument_Associations (Prag));
- Arg2 := Next (Arg1);
- Arg3 := Next (Arg2);
-
- Arg1 := Get_Pragma_Arg (Arg1);
- Arg2 := Get_Pragma_Arg (Arg2);
-
- -- The caller requests processing of all Invariant'Class pragmas,
- -- but the current pragma does not fall in this category. Return
- -- as there is nothing left to do.
-
- if Inherit then
- if not Class_Present (Prag) then
- return;
- end if;
-
- -- Otherwise the pragma must apply to the current type
-
- elsif Entity (Arg1) /= T then
- return;
- end if;
-
- Expr := New_Copy_Tree (Arg2);
-
- -- Replace all occurrences of the type's name with references to
- -- the formal parameter of the invariant procedure.
-
- Replace_Type_References (Expr, T);
-
- -- If the invariant pragma comes from an aspect, replace the saved
- -- expression because we need the subtype references replaced for
- -- the calls to Preanalyze_Spec_Expression in Check_Aspect_At_xxx
- -- routines. This is not done for interited class-wide invariants
- -- because the original pragma of the parent type must remain
- -- unchanged.
-
- if not Inherit and then Present (Asp) then
- Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
- end if;
-
- -- Preanalyze the invariant expression to capture the visibility
- -- of the proper package part. In general the expression is not
- -- fully analyzed until the body of the invariant procedure is
- -- analyzed at the end of the private part, but that yields the
- -- wrong visibility.
-
- -- Historical note: we used to set N as the parent, but a package
- -- specification as the parent of an expression is bizarre.
-
- Set_Parent (Expr, Parent (Arg2));
- Preanalyze_Assert_Expression (Expr, Any_Boolean);
-
- -- Both modifications performed below are not done for inherited
- -- class-wide invariants because the origial aspect/pragma of the
- -- parent type must remain unchanged.
-
- if not Inherit then
-
- -- A class-wide invariant may be inherited in a separate unit,
- -- where the corresponding expression cannot be resolved by
- -- visibility, because it refers to a local function. Propagate
- -- semantic information to the original representation item, to
- -- be used when an invariant procedure for a derived type is
- -- constructed.
-
- -- ??? Unclear how to handle class-wide invariants that are not
- -- function calls.
-
- if Class_Present (Prag)
- and then Nkind (Expr) = N_Function_Call
- and then Nkind (Arg2) = N_Indexed_Component
- then
- Rewrite (Arg2,
- Make_Function_Call (Ploc,
- Name =>
- New_Occurrence_Of (Entity (Name (Expr)), Ploc),
- Parameter_Associations => Expressions (Arg2)));
- end if;
-
- -- In ASIS mode, even if assertions are not enabled, we must
- -- analyze the original expression in the aspect specification
- -- because it is part of the original tree.
-
- if ASIS_Mode and then Present (Asp) then
- declare
- Asp_Expr : constant Node_Id := Expression (Asp);
-
- begin
- Replace_Type_References (Asp_Expr, T);
- Preanalyze_Assert_Expression (Asp_Expr, Any_Boolean);
- end;
- end if;
- end if;
-
- -- An ignored invariant must not generate a runtime check. Add a
- -- null statement to ensure that the invariant procedure does get
- -- a completing body.
-
- if No (Stmts) then
- Stmts := Empty_List;
- end if;
-
- if Is_Ignored (Prag) then
- Append_To (Stmts, Make_Null_Statement (Ploc));
-
- -- Otherwise the invariant is checked. Build a Check pragma to
- -- verify the expression at runtime.
-
- else
- Assoc := New_List (
- Make_Pragma_Argument_Association (Ploc,
- Expression => Make_Identifier (Ploc, Nam)),
- Make_Pragma_Argument_Association (Ploc,
- Expression => Expr));
-
- -- Handle the String argument (if any)
-
- if Present (Arg3) then
- Str := Strval (Get_Pragma_Arg (Arg3));
-
- -- When inheriting an invariant, modify the message from
- -- "failed invariant" to "failed inherited invariant".
-
- if Inherit then
- String_To_Name_Buffer (Str);
-
- if Name_Buffer (1 .. 16) = "failed invariant" then
- Insert_Str_In_Name_Buffer ("inherited ", 8);
- Str := String_From_Name_Buffer;
- end if;
- end if;
-
- Append_To (Assoc,
- Make_Pragma_Argument_Association (Ploc,
- Expression => Make_String_Literal (Ploc, Str)));
- end if;
-
- -- Generate:
- -- pragma Check (Nam, Expr, Str);
-
- Append_To (Stmts,
- Make_Pragma (Ploc,
- Pragma_Identifier =>
- Make_Identifier (Ploc, Name_Check),
- Pragma_Argument_Associations => Assoc));
- end if;
-
- -- Output an info message when inheriting an invariant and the
- -- listing option is enabled.
-
- if Inherit and Opt.List_Inherited_Aspects then
- Error_Msg_Sloc := Sloc (Prag);
- Error_Msg_N
- ("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
- end if;
- end Add_Invariant;
-
- -- Local variables
-
- Ritem : Node_Id;
-
- -- Start of processing for Add_Invariants
-
- begin
- Ritem := First_Rep_Item (T);
- while Present (Ritem) loop
- if Nkind (Ritem) = N_Pragma
- and then Pragma_Name (Ritem) = Name_Invariant
- then
- Add_Invariant (Ritem);
- end if;
-
- Next_Rep_Item (Ritem);
- end loop;
- end Add_Invariants;
-
- -- Local variables
-
- Loc : constant Source_Ptr := Sloc (Typ);
- Priv_Decls : constant List_Id := Private_Declarations (N);
- Vis_Decls : constant List_Id := Visible_Declarations (N);
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
- PBody : Node_Id;
- PDecl : Node_Id;
- SId : Entity_Id;
- Spec : Node_Id;
- Stmts : List_Id;
-
- Obj_Id : Node_Id;
- -- The entity of the formal for the procedure
-
- -- Start of processing for Build_Invariant_Procedure
-
- begin
- -- The related type may be subject to pragma Ghost. Set the mode now to
- -- ensure that the invariant procedure is properly marked as Ghost.
-
- Set_Ghost_Mode_From_Entity (Typ);
-
- Stmts := No_List;
- PDecl := Empty;
- PBody := Empty;
- 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 the body is already present, nothing to do. This will occur when
- -- the type is already frozen, which is the case when the invariant
- -- appears in a private part, and the freezing takes place before the
- -- final pass over full declarations.
-
- -- See Exp_Ch3.Insert_Component_Invariant_Checks for details.
-
- if Present (SId) then
- PDecl := Unit_Declaration_Node (SId);
-
- if Present (PDecl)
- and then Nkind (PDecl) = N_Subprogram_Declaration
- and then Present (Corresponding_Body (PDecl))
- then
- Ghost_Mode := Save_Ghost_Mode;
- return;
- end if;
-
- else
- PDecl := Build_Invariant_Procedure_Declaration (Typ);
- end if;
-
- -- Recover formal of procedure, for use in the calls to invariant
- -- functions (including inherited ones).
-
- Obj_Id :=
- Defining_Identifier
- (First (Parameter_Specifications (Specification (PDecl))));
-
- -- Add invariants for the current type
-
- Add_Invariants
- (T => Typ,
- Obj_Id => Obj_Id,
- Stmts => Stmts,
- Inherit => False);
-
- -- Add invariants for parent types
-
- declare
- Current_Typ : Entity_Id;
- Parent_Typ : Entity_Id;
-
- begin
- Current_Typ := Typ;
- loop
- Parent_Typ := Etype (Current_Typ);
-
- if Is_Private_Type (Parent_Typ)
- and then Present (Full_View (Base_Type (Parent_Typ)))
- then
- Parent_Typ := Full_View (Base_Type (Parent_Typ));
- end if;
-
- exit when Parent_Typ = Current_Typ;
-
- Current_Typ := Parent_Typ;
- Add_Invariants
- (T => Current_Typ,
- Obj_Id => Obj_Id,
- Stmts => Stmts,
- Inherit => True);
- end loop;
- end;
-
- -- Add invariants of progenitors
-
- if Is_Tagged_Type (Typ) and then not Is_Interface (Typ) then
- declare
- Ifaces_List : Elist_Id;
- AI : Elmt_Id;
- Iface : Entity_Id;
-
- begin
- Collect_Interfaces (Typ, Ifaces_List);
-
- AI := First_Elmt (Ifaces_List);
- while Present (AI) loop
- Iface := Node (AI);
-
- if not Is_Ancestor (Iface, Typ, Use_Full_View => True) then
- Add_Invariants
- (T => Iface,
- Obj_Id => Obj_Id,
- Stmts => Stmts,
- Inherit => True);
- end if;
-
- Next_Elmt (AI);
- end loop;
- end;
- end if;
-
- -- Build the procedure if we generated at least one Check pragma
-
- if Stmts /= No_List then
- Spec := Copy_Separate_Tree (Specification (PDecl));
-
- PBody :=
- Make_Subprogram_Body (Loc,
- Specification => Spec,
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Stmts));
-
- -- The processing of an invariant pragma immediately generates the
- -- invariant procedure spec, inserts it into the tree, and analyzes
- -- it. If the spec has not been analyzed, then the invariant pragma
- -- is being inherited and requires manual insertion and analysis.
-
- if not Analyzed (PDecl) then
- Append_To (Vis_Decls, PDecl);
- Analyze (PDecl);
- end if;
-
- -- The invariant procedure body is inserted at the end of the private
- -- declarations.
-
- if Present (Priv_Decls) then
- Append_To (Priv_Decls, PBody);
-
- -- If the invariant appears on the full view of a private type,
- -- then the analysis of the private part is already completed.
- -- Manually analyze the new body in this case, otherwise wait
- -- for the analysis of the private declarations to process the
- -- body.
-
- if In_Private_Part (Current_Scope) then
- Analyze (PBody);
- end if;
-
- -- Otherwise there are no private declarations. This is either an
- -- error or the related type is a private extension, in which case
- -- it does not need a completion in a private part. Insert the body
- -- at the end of the visible declarations and analyze immediately
- -- because the related type is about to be frozen.
-
- else
- Append_To (Vis_Decls, PBody);
- Analyze (PBody);
- end if;
- end if;
-
- Ghost_Mode := Save_Ghost_Mode;
- end Build_Invariant_Procedure;
-
- -------------------------------
-- Build_Predicate_Functions --
-------------------------------
@@ -11159,9 +10588,7 @@
end if;
end Hide_Non_Overridden_Subprograms;
- ---------------------
- -- Local variables --
- ---------------------
+ -- Local variables
E : constant Entity_Id := Entity (N);
@@ -11324,14 +10751,14 @@
Inside_Freezing_Actions := Inside_Freezing_Actions - 1;
- -- If we have a type with predicates, build predicate function. This
- -- is not needed in the generic case, and is not needed within TSS
- -- subprograms and other predefined primitives.
+ -- If we have a type with predicates, build predicate function. This is
+ -- not needed in the generic case, nor within TSS subprograms and other
+ -- predefined primitives.
- if Non_Generic_Case
- and then Is_Type (E)
- and then Has_Predicates (E)
+ if Is_Type (E)
+ and then Non_Generic_Case
and then not Within_Internal_Subprogram
+ and then Has_Predicates (E)
then
Build_Predicate_Functions (E, N);
end if;
@@ -11830,30 +11257,6 @@
Set_Discard_Names (Typ);
end if;
- -- Invariants
-
- if not Has_Rep_Item (Typ, Name_Invariant, False)
- and then Has_Rep_Item (Typ, Name_Invariant)
- and then Is_Pragma_Or_Corr_Pragma_Present_In_Rep_Item
- (Get_Rep_Item (Typ, Name_Invariant))
- then
- Set_Has_Invariants (Typ);
-
- if Class_Present (Get_Rep_Item (Typ, Name_Invariant)) then
- Set_Has_Inheritable_Invariants (Typ);
- end if;
-
- -- If we have a subtype with invariants, whose base type does not have
- -- invariants, copy these invariants to the base type. This happens for
- -- the case of implicit base types created for scalar and array types.
-
- elsif Has_Invariants (Typ)
- and then not Has_Invariants (Base_Type (Typ))
- then
- Set_Has_Invariants (Base_Type (Typ));
- Set_Invariant_Procedure (Base_Type (Typ), Invariant_Procedure (Typ));
- end if;
-
-- Volatile
if not Has_Rep_Item (Typ, Name_Volatile, False)
@@ -12636,7 +12039,7 @@
if Has_Discriminants (E) then
Push_Scope (E);
- -- Make discriminants visible for type declarations and protected
+ -- Make the discriminants visible for type declarations and protected
-- type declarations, not for subtype declarations (RM 13.1.1 (12/3))
if Nkind (Parent (E)) /= N_Subtype_Declaration then
@@ -12891,18 +12294,15 @@
procedure Replace_Type_References_Generic (N : Node_Id; T : Entity_Id) is
TName : constant Name_Id := Chars (T);
- function Replace_Node (N : Node_Id) return Traverse_Result;
+ function Replace_Type_Ref (N : Node_Id) return Traverse_Result;
-- Processes a single node in the traversal procedure below, checking
-- if node N should be replaced, and if so, doing the replacement.
- procedure Replace_Type_Refs is new Traverse_Proc (Replace_Node);
- -- This instantiation provides the body of Replace_Type_References
+ ----------------------
+ -- Replace_Type_Ref --
+ ----------------------
- ------------------
- -- Replace_Node --
- ------------------
-
- function Replace_Node (N : Node_Id) return Traverse_Result is
+ function Replace_Type_Ref (N : Node_Id) return Traverse_Result is
S : Entity_Id;
P : Node_Id;
@@ -12911,10 +12311,10 @@
if Nkind (N) = N_Identifier then
- -- If not the type name, check whether it is a reference to
- -- some other type, which must be frozen before the predicate
- -- function is analyzed, i.e. before the freeze node of the
- -- type to which the predicate applies.
+ -- If not the type name, check whether it is a reference to some
+ -- other type, which must be frozen before the predicate function
+ -- is analyzed, i.e. before the freeze node of the type to which
+ -- the predicate applies.
if Chars (N) /= TName then
if Present (Current_Entity (N))
@@ -12932,13 +12332,13 @@
return Skip;
end if;
- -- Case of selected component (which is what a qualification
- -- looks like in the unanalyzed tree, which is what we have.
+ -- Case of selected component (which is what a qualification looks
+ -- like in the unanalyzed tree, which is what we have.
elsif Nkind (N) = N_Selected_Component then
- -- If selector name is not our type, keeping going (we might
- -- still have an occurrence of the type in the prefix).
+ -- If selector name is not our type, keeping going (we might still
+ -- have an occurrence of the type in the prefix).
if Nkind (Selector_Name (N)) /= N_Identifier
or else Chars (Selector_Name (N)) /= TName
@@ -12959,8 +12359,8 @@
return OK;
end if;
- -- Do replace if prefix is an identifier matching the
- -- scope that we are currently looking at.
+ -- Do replace if prefix is an identifier matching the scope
+ -- that we are currently looking at.
if Nkind (P) = N_Identifier
and then Chars (P) = Chars (S)
@@ -12969,9 +12369,9 @@
return Skip;
end if;
- -- Go check scope above us if prefix is itself of the
- -- form of a selected component, whose selector matches
- -- the scope we are currently looking at.
+ -- Go check scope above us if prefix is itself of the form
+ -- of a selected component, whose selector matches the scope
+ -- we are currently looking at.
if Nkind (P) = N_Selected_Component
and then Nkind (Selector_Name (P)) = N_Identifier
@@ -12995,8 +12395,10 @@
else
return OK;
end if;
- end Replace_Node;
+ end Replace_Type_Ref;
+ procedure Replace_Type_Refs is new Traverse_Proc (Replace_Type_Ref);
+
begin
Replace_Type_Refs (N);
end Replace_Type_References_Generic;
@@ -13057,17 +12459,18 @@
Expr := Expression (ASN);
case A_Id is
+
-- For now we only deal with aspects that do not generate
-- subprograms, or that may mention current instances of
-- types. These will require special handling (???TBD).
when Aspect_Predicate |
Aspect_Predicate_Failure |
- Aspect_Invariant =>
+ Aspect_Invariant =>
null;
- when Aspect_Static_Predicate |
- Aspect_Dynamic_Predicate =>
+ when Aspect_Dynamic_Predicate |
+ Aspect_Static_Predicate =>
-- Build predicate function specification and preanalyze
-- expression after type replacement.
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -53,25 +53,6 @@
-- 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
- -- rep chain, note that Invariant aspects have already been converted to
- -- pragma Invariant), then this procedure builds the spec and body for the
- -- corresponding Invariant procedure, inserting them at appropriate points
- -- in the package specification N. Invariant_Procedure is set for Typ. Note
- -- that this procedure is called at the end of processing the declarations
- -- in the visible part (i.e. the right point for visibility analysis of
- -- the invariant expression).
-
procedure Check_Record_Representation_Clause (N : Node_Id);
-- This procedure completes the analysis of a record representation clause
-- N. It is called at freeze time after adjustment of component clause bit
===================================================================
@@ -6,7 +6,7 @@
* *
* C Header File *
* *
- * Copyright (C) 1992-2015, Free Software Foundation, Inc. *
+ * Copyright (C) 1992-2016, Free Software Foundation, Inc. *
* *
* GNAT is free software; you can redistribute it and/or modify it under *
* terms of the GNU General Public License as published by the Free Soft- *
@@ -526,6 +526,7 @@
#define Elist24(N) Field24 (N)
#define Elist25(N) Field25 (N)
#define Elist26(N) Field26 (N)
+#define Elist29(N) Field29 (N)
#define Elist36(N) Field36 (N)
#define Name1(N) Field1 (N)
===================================================================
@@ -59,7 +59,6 @@
with Sem_Ch3; use Sem_Ch3;
with Sem_Ch6; use Sem_Ch6;
with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
with Sem_Mech; use Sem_Mech;
@@ -92,22 +91,6 @@
-- used for attachment of any actions required in its construction.
-- It also supplies the source location used for the procedure.
- function Build_Array_Invariant_Proc
- (A_Type : Entity_Id;
- Nod : Node_Id) return Node_Id;
- -- If the component of type of array type has invariants, build procedure
- -- that checks invariant on all components of the array. Ada 2012 specifies
- -- that an invariant on some type T must be applied to in-out parameters
- -- and return values that include a part of type T. If the array type has
- -- an otherwise specified invariant, the component check procedure is
- -- called from within the user-specified invariant. Otherwise this becomes
- -- the invariant procedure for the array type.
-
- function Build_Record_Invariant_Proc
- (R_Type : Entity_Id;
- Nod : Node_Id) return Node_Id;
- -- Ditto for record types.
-
function Build_Discriminant_Formals
(Rec_Id : Entity_Id;
Use_Dl : Boolean) return List_Id;
@@ -200,14 +183,6 @@
-- Treat user-defined stream operations as renaming_as_body if the
-- subprogram they rename is not frozen when the type is frozen.
- procedure Insert_Component_Invariant_Checks
- (N : Node_Id;
- Typ : Entity_Id;
- Proc : Node_Id);
- -- If a composite type has invariants and also has components with defined
- -- invariants. the component invariant procedure is inserted into the user-
- -- defined invariant procedure and added to the checks to be performed.
-
procedure Initialization_Warning (E : Entity_Id);
-- If static elaboration of the package is requested, indicate
-- when a type does meet the conditions for static initialization. If
@@ -795,138 +770,6 @@
end Build_Array_Init_Proc;
--------------------------------
- -- Build_Array_Invariant_Proc --
- --------------------------------
-
- function Build_Array_Invariant_Proc
- (A_Type : Entity_Id;
- Nod : Node_Id) return Node_Id
- is
- Loc : constant Source_Ptr := Sloc (Nod);
-
- Object_Name : constant Name_Id := New_Internal_Name ('I');
- -- Name for argument of invariant procedure
-
- Object_Entity : constant Node_Id :=
- Make_Defining_Identifier (Loc, Object_Name);
- -- The procedure declaration entity for the argument
-
- Body_Stmts : List_Id;
- Index_List : List_Id;
- Proc_Id : Entity_Id;
- Proc_Body : Node_Id;
-
- function Build_Component_Invariant_Call return Node_Id;
- -- Create one statement to verify invariant on one array component,
- -- designated by a full set of indexes.
-
- function Check_One_Dimension (N : Int) return List_Id;
- -- Create loop to check on one dimension of the array. The single
- -- statement in the loop body checks the inner dimensions if any, or
- -- else a single component. This procedure is called recursively, with
- -- N being the dimension to be initialized. A call with N greater than
- -- the number of dimensions generates the component initialization
- -- and terminates the recursion.
-
- ------------------------------------
- -- Build_Component_Invariant_Call --
- ------------------------------------
-
- function Build_Component_Invariant_Call return Node_Id is
- Comp : Node_Id;
- begin
- Comp :=
- Make_Indexed_Component (Loc,
- Prefix => New_Occurrence_Of (Object_Entity, Loc),
- Expressions => Index_List);
- return
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Invariant_Procedure (Component_Type (A_Type)), Loc),
- Parameter_Associations => New_List (Comp));
- end Build_Component_Invariant_Call;
-
- -------------------------
- -- Check_One_Dimension --
- -------------------------
-
- function Check_One_Dimension (N : Int) return List_Id is
- Index : Entity_Id;
-
- begin
- -- If all dimensions dealt with, we simply check invariant of the
- -- component.
-
- if N > Number_Dimensions (A_Type) then
- return New_List (Build_Component_Invariant_Call);
-
- -- Else generate one loop and recurse
-
- else
- Index :=
- Make_Defining_Identifier (Loc, New_External_Name ('J', N));
-
- Append (New_Occurrence_Of (Index, Loc), Index_List);
-
- return New_List (
- Make_Implicit_Loop_Statement (Nod,
- Identifier => Empty,
- Iteration_Scheme =>
- Make_Iteration_Scheme (Loc,
- Loop_Parameter_Specification =>
- Make_Loop_Parameter_Specification (Loc,
- Defining_Identifier => Index,
- Discrete_Subtype_Definition =>
- Make_Attribute_Reference (Loc,
- Prefix =>
- New_Occurrence_Of (Object_Entity, Loc),
- Attribute_Name => Name_Range,
- Expressions => New_List (
- Make_Integer_Literal (Loc, N))))),
- Statements => Check_One_Dimension (N + 1)));
- end if;
- end Check_One_Dimension;
-
- -- Start of processing for Build_Array_Invariant_Proc
-
- begin
- Index_List := New_List;
-
- Proc_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (A_Type), "CInvariant"));
-
- Body_Stmts := Check_One_Dimension (1);
-
- Proc_Body :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Proc_Id,
- Parameter_Specifications => New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Object_Entity,
- Parameter_Type => New_Occurrence_Of (A_Type, Loc)))),
-
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Body_Stmts));
-
- Set_Ekind (Proc_Id, E_Procedure);
- Set_Is_Public (Proc_Id, Is_Public (A_Type));
- Set_Is_Internal (Proc_Id);
- Set_Has_Completion (Proc_Id);
-
- if not Debug_Generated_Code then
- Set_Debug_Info_Off (Proc_Id);
- end if;
-
- return Proc_Body;
- end Build_Array_Invariant_Proc;
-
- --------------------------------
-- Build_Discr_Checking_Funcs --
--------------------------------
@@ -3671,242 +3514,6 @@
end if;
end Build_Record_Init_Proc;
- --------------------------------
- -- Build_Record_Invariant_Proc --
- --------------------------------
-
- function Build_Record_Invariant_Proc
- (R_Type : Entity_Id;
- Nod : Node_Id) return Node_Id
- is
- Loc : constant Source_Ptr := Sloc (Nod);
-
- Object_Name : constant Name_Id := New_Internal_Name ('I');
- -- Name for argument of invariant procedure
-
- Object_Entity : constant Node_Id :=
- Make_Defining_Identifier (Loc, Object_Name);
- -- The procedure declaration entity for the argument
-
- Invariant_Found : Boolean;
- -- Set if any component needs an invariant check.
-
- Proc_Id : Entity_Id;
- Proc_Body : Node_Id;
- Stmts : List_Id;
- Type_Def : Node_Id;
-
- function Build_Invariant_Checks (Comp_List : Node_Id) return List_Id;
- -- Recursive procedure that generates a list of checks for components
- -- that need it, and recurses through variant parts when present.
-
- function Build_Component_Invariant_Call
- (Comp : Entity_Id) return Node_Id;
- -- Build call to invariant procedure for a record component
-
- ------------------------------------
- -- Build_Component_Invariant_Call --
- ------------------------------------
-
- function Build_Component_Invariant_Call
- (Comp : Entity_Id) return Node_Id
- is
- Call : Node_Id;
- Proc : Entity_Id;
- Sel_Comp : Node_Id;
- Typ : Entity_Id;
-
- begin
- Typ := Etype (Comp);
-
- Sel_Comp :=
- Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (Object_Entity, Loc),
- Selector_Name => New_Occurrence_Of (Comp, Loc));
-
- if Is_Access_Type (Typ) then
-
- -- If the access component designates a type with an invariant,
- -- the check applies to the designated object. The access type
- -- itself may have an invariant, in which case it applies to the
- -- access value directly.
-
- -- Note: we are assuming that invariants will not occur on both
- -- the access type and the type that it designates. This is not
- -- really justified but it is hard to imagine that this case will
- -- ever cause trouble ???
-
- if not (Has_Invariants (Typ)) then
- Sel_Comp := Make_Explicit_Dereference (Loc, Sel_Comp);
- Typ := Designated_Type (Typ);
- end if;
- end if;
-
- -- The aspect is type-specific, so retrieve it from the base type
-
- Proc := Invariant_Procedure (Base_Type (Typ));
-
- if Has_Null_Body (Proc) then
- return Make_Null_Statement (Loc);
- end if;
-
- Invariant_Found := True;
- Call :=
- Make_Procedure_Call_Statement (Loc,
- Name => New_Occurrence_Of (Proc, Loc),
- Parameter_Associations => New_List (Sel_Comp));
-
- if Is_Access_Type (Etype (Comp)) then
- Call :=
- Make_If_Statement (Loc,
- Condition =>
- Make_Op_Ne (Loc,
- Left_Opnd => Make_Null (Loc),
- Right_Opnd =>
- Make_Selected_Component (Loc,
- Prefix =>
- New_Occurrence_Of (Object_Entity, Loc),
- Selector_Name => New_Occurrence_Of (Comp, Loc))),
- Then_Statements => New_List (Call));
- end if;
-
- return Call;
- end Build_Component_Invariant_Call;
-
- ----------------------------
- -- Build_Invariant_Checks --
- ----------------------------
-
- function Build_Invariant_Checks (Comp_List : Node_Id) return List_Id is
- Decl : Node_Id;
- Id : Entity_Id;
- Stmts : List_Id;
-
- begin
- Stmts := New_List;
- Decl := First_Non_Pragma (Component_Items (Comp_List));
- while Present (Decl) loop
- if Nkind (Decl) = N_Component_Declaration then
- Id := Defining_Identifier (Decl);
-
- if Has_Invariants (Etype (Id))
- and then In_Open_Scopes (Scope (R_Type))
- then
- if Has_Unchecked_Union (R_Type) then
- Error_Msg_NE
- ("invariants cannot be checked on components of "
- & "unchecked_union type&?", Decl, R_Type);
- return Empty_List;
-
- else
- Append_To (Stmts, Build_Component_Invariant_Call (Id));
- end if;
-
- elsif Is_Access_Type (Etype (Id))
- and then not Is_Access_Constant (Etype (Id))
- and then Has_Invariants (Designated_Type (Etype (Id)))
- and then In_Open_Scopes (Scope (Designated_Type (Etype (Id))))
- then
- Append_To (Stmts, Build_Component_Invariant_Call (Id));
- end if;
- end if;
-
- Next (Decl);
- end loop;
-
- if Present (Variant_Part (Comp_List)) then
- declare
- Variant_Alts : constant List_Id := New_List;
- Var_Loc : Source_Ptr;
- Variant : Node_Id;
- Variant_Stmts : List_Id;
-
- begin
- Variant :=
- First_Non_Pragma (Variants (Variant_Part (Comp_List)));
- while Present (Variant) loop
- Variant_Stmts :=
- Build_Invariant_Checks (Component_List (Variant));
- Var_Loc := Sloc (Variant);
- Append_To (Variant_Alts,
- Make_Case_Statement_Alternative (Var_Loc,
- Discrete_Choices =>
- New_Copy_List (Discrete_Choices (Variant)),
- Statements => Variant_Stmts));
-
- Next_Non_Pragma (Variant);
- end loop;
-
- -- The expression in the case statement is the reference to
- -- the discriminant of the target object.
-
- Append_To (Stmts,
- Make_Case_Statement (Var_Loc,
- Expression =>
- Make_Selected_Component (Var_Loc,
- Prefix => New_Occurrence_Of (Object_Entity, Var_Loc),
- Selector_Name => New_Occurrence_Of
- (Entity
- (Name (Variant_Part (Comp_List))), Var_Loc)),
- Alternatives => Variant_Alts));
- end;
- end if;
-
- return Stmts;
- end Build_Invariant_Checks;
-
- -- Start of processing for Build_Record_Invariant_Proc
-
- begin
- Invariant_Found := False;
- Type_Def := Type_Definition (Parent (R_Type));
-
- if Nkind (Type_Def) = N_Record_Definition
- and then not Null_Present (Type_Def)
- then
- Stmts := Build_Invariant_Checks (Component_List (Type_Def));
- else
- return Empty;
- end if;
-
- if not Invariant_Found then
- return Empty;
- end if;
-
- -- The name of the invariant procedure reflects the fact that the
- -- checks correspond to invariants on the component types. The
- -- record type itself may have invariants that will create a separate
- -- procedure whose name carries the Invariant suffix.
-
- Proc_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (R_Type), "CInvariant"));
-
- Proc_Body :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Proc_Id,
- Parameter_Specifications => New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Object_Entity,
- Parameter_Type => New_Occurrence_Of (R_Type, Loc)))),
-
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Stmts));
-
- Set_Ekind (Proc_Id, E_Procedure);
- Set_Is_Public (Proc_Id, Is_Public (R_Type));
- Set_Is_Internal (Proc_Id);
- Set_Has_Completion (Proc_Id);
-
- return Proc_Body;
- -- Insert_After (Nod, Proc_Body);
- -- Analyze (Proc_Body);
- end Build_Record_Invariant_Proc;
-
----------------------------
-- Build_Slice_Assignment --
----------------------------
@@ -4680,21 +4287,6 @@
Build_Array_Init_Proc (Base, N);
end if;
- if Has_Invariants (Component_Type (Base))
- and then Typ = Base
- and then In_Open_Scopes (Scope (Component_Type (Base)))
- then
- -- Generate component invariant checking procedure. This is only
- -- relevant if the array type is within the scope of the component
- -- type. Otherwise an array object can only be built using the public
- -- subprograms for the component type, and calls to those will have
- -- invariant checks. The invariant procedure is only generated for
- -- a base type, not a subtype.
-
- Insert_Component_Invariant_Checks
- (N, Base, Build_Array_Invariant_Proc (Base, N));
- end if;
-
Ghost_Mode := Save_Ghost_Mode;
end Expand_Freeze_Array_Type;
@@ -5551,24 +5143,6 @@
end;
end if;
- -- Check whether individual components have a defined invariant, and add
- -- the corresponding component invariant checks.
-
- -- Do not create an invariant procedure for some internally generated
- -- subtypes, in particular those created for objects of a class-wide
- -- type. Such types may have components to which invariant apply, but
- -- the corresponding checks will be applied when an object of the parent
- -- type is constructed.
-
- -- Such objects will show up in a class-wide postcondition, and the
- -- invariant will be checked, if necessary, upon return from the
- -- enclosing subprogram.
-
- if not Is_Class_Wide_Equivalent_Type (Typ) then
- Insert_Component_Invariant_Checks
- (N, Typ, Build_Record_Invariant_Proc (Typ, N));
- end if;
-
Ghost_Mode := Save_Ghost_Mode;
end Expand_Freeze_Record_Type;
@@ -7476,11 +7050,11 @@
elsif Ekind_In (Def_Id, E_Access_Type, E_General_Access_Type) then
declare
- Loc : constant Source_Ptr := Sloc (N);
- Desig_Type : constant Entity_Id := Designated_Type (Def_Id);
- Pool_Object : Entity_Id;
+ Loc : constant Source_Ptr := Sloc (N);
+ Desig_Type : constant Entity_Id := Designated_Type (Def_Id);
Freeze_Action_Typ : Entity_Id;
+ Pool_Object : Entity_Id;
begin
-- Case 1
@@ -7500,8 +7074,8 @@
elsif Has_Storage_Size_Clause (Def_Id) then
declare
- DT_Size : Node_Id;
DT_Align : Node_Id;
+ DT_Size : Node_Id;
begin
-- For unconstrained composite types we give a size of zero
@@ -7746,6 +7320,16 @@
Process_Pending_Access_Types (Def_Id);
Freeze_Stream_Operations (N, Def_Id);
+ -- Generate the [spec and] body of the invariant procedure tasked with
+ -- the runtime verification of all invariants that pertain to the type.
+ -- This includes invariants on the partial and full view, inherited
+ -- class-wide invariants from parent types or interfaces, and invariants
+ -- on array elements or record components.
+
+ if Has_Invariants (Def_Id) then
+ Build_Invariant_Procedure_Body (Def_Id);
+ end if;
+
Ghost_Mode := Save_Ghost_Mode;
return Result;
@@ -8164,77 +7748,6 @@
return Is_RTU (S1, System) or else Is_RTU (S1, Ada);
end In_Runtime;
- ---------------------------------------
- -- Insert_Component_Invariant_Checks --
- ---------------------------------------
-
- procedure Insert_Component_Invariant_Checks
- (N : Node_Id;
- Typ : Entity_Id;
- Proc : Node_Id)
- is
- Loc : constant Source_Ptr := Sloc (Typ);
- Proc_Id : Entity_Id;
-
- begin
- if Present (Proc) then
- Proc_Id := Defining_Entity (Proc);
-
- if not Has_Invariants (Typ) then
- Set_Has_Invariants (Typ);
- Set_Is_Invariant_Procedure (Proc_Id);
- Set_Invariant_Procedure (Typ, Proc_Id);
- Insert_After (N, Proc);
- Analyze (Proc);
-
- else
-
- -- Find already created invariant subprogram, insert body of
- -- component invariant proc in its body, and add call after
- -- other checks.
-
- declare
- Bod : Node_Id;
- Inv_Id : constant Entity_Id := Invariant_Procedure (Typ);
- Call : constant Node_Id :=
- Make_Procedure_Call_Statement (Sloc (N),
- Name => New_Occurrence_Of (Proc_Id, Loc),
- Parameter_Associations =>
- New_List
- (New_Occurrence_Of (First_Formal (Inv_Id), Loc)));
-
- begin
- -- The invariant body has not been analyzed yet, so we do a
- -- sequential search forward, and retrieve it by name.
-
- Bod := Next (N);
- while Present (Bod) loop
- exit when Nkind (Bod) = N_Subprogram_Body
- and then Chars (Defining_Entity (Bod)) = Chars (Inv_Id);
- Next (Bod);
- end loop;
-
- -- If the body is not found, it is the case of an invariant
- -- appearing on a full declaration in a private part, in
- -- which case the type has been frozen but the invariant
- -- procedure for the composite type not created yet. Create
- -- body now.
-
- if No (Bod) then
- Build_Invariant_Procedure (Typ, Parent (Current_Scope));
- Bod := Unit_Declaration_Node
- (Corresponding_Body (Unit_Declaration_Node (Inv_Id)));
- end if;
-
- Append_To (Declarations (Bod), Proc);
- Append_To (Statements (Handled_Statement_Sequence (Bod)), Call);
- Analyze (Proc);
- Analyze (Call);
- end;
- end if;
- end if;
- end Insert_Component_Invariant_Checks;
-
----------------------------
-- Initialization_Warning --
----------------------------
This patch reimplements the processing of type invariants in order to plug various static and run-time semantic holes. The invariants of a private type are resolved and checked at run-time by a "partial" invariant procedure. The invariants of a private type's full view, any inherited class-wide invariants of parent types or interfaces, any invariants on array elements or record components, and the invariants of the partial view are resolved and checked at run-time by a "full" invariant procedure. ------------ -- Source -- ------------ -- tester.ads package Tester is type Type_Id is (Ext_1_Id, Ext_1_FV_Id, Ext_2_Id, Ext_3_Id, Ext_4_Id, Ext_4_FV_Id, Ext_5_Id, Ext_6_Id, Ext_6_FV_Id, Ext_7_Id, Ext_8_Id, Iface_1_Id, Iface_2_Id, Iface_3_Id, Iface_4_Id, Par_1_Id, Par_2_FV_Id, Par_3_Id, Par_4_Id, Par_4_FV_Id, Prot_1_FV_Id, Prot_2_Id, Prot_3_Id, Prot_3_FV_Id, Synch_1_Id, Synch_2_Id, Tag_1_Id, Tag_2_Id, Tag_3_Id, Tag_4_Id, Tag_4_FV_Id, Tag_5_Id, Tag_6_Id, Tag_7_Id, Tag_8_Id, Tag_9_Id, Tag_10_Id, Tag_11_Id, Tag_12_Id, Tag_13_Id, Tag_14_Id, Tag_15_Id, Tag_15_FV_Id, Tag_16_Id, Tag_17_Id, Tag_18_Id, Tag_19_Id, Tag_20_Id, Tag_20_FV_Id, Tag_21_Id, Tag_22_Id, Tag_23_Id, Tag_24_Id, Tag_24_FV_Id, Tag_25_Id, Tag_26_Id, Tag_27_Id, Tag_28_Id, Task_1_Id, Task_2_Id, Task_2_FV_Id, Untag_1_Id, Untag_2_Id, Untag_3_Id, Untag_4_Id, Untag_5_Id, Untag_6_Id, Untag_7_Id, Untag_8_Id, Untag_9_Id); type Results is array (Type_Id) of Boolean; function Mark (Typ : Type_Id) return Boolean; -- Mark the result for a particular type as verified. The function always -- returns True. procedure Reset_Results; -- Reset the internally kept result state procedure Test_Results (Test_Id : String; Exp : Results); -- Ensure that the internally kept result state agrees with expected -- results Exp. Emit an error if this is not the case. end Tester; -- tester.adb with Ada.Text_IO; use Ada.Text_IO; package body Tester is State : Results; ---------- -- Mark -- ---------- function Mark (Typ : Type_Id) return Boolean is begin State (Typ) := True; return True; end Mark; ------------------- -- Reset_Results -- ------------------- procedure Reset_Results is begin State := (others => False); end Reset_Results; ------------------ -- Test_Results -- ------------------ procedure Test_Results (Test_Id : String; Exp : Results) is Exp_Val : Boolean; Posted : Boolean := False; State_Val : Boolean; begin for Index in Results'Range loop Exp_Val := Exp (Index); State_Val := State (Index); if State_Val /= Exp_Val then if not Posted then Posted := True; Put_Line (Test_Id & ": ERROR"); end if; Put_Line (" Expected: " & Exp_Val'Img & " for " & Index'Img); Put_Line (" Got: " & State_Val'Img); end if; end loop; if not Posted then Put_Line (Test_Id & ": OK"); end if; end Test_Results; end Tester; -- invariants_aspects.ads with Tester; use Tester; package Invariants_Aspects is ---------------- -- Interfaces -- ---------------- type Iface_1 is interface with Type_Invariant'Class => Mark (Iface_1_Id); type Iface_2 is interface with Type_Invariant'Class => Mark (Iface_2_Id); type Iface_3 is interface and Iface_1 and Iface_2; type Iface_4 is interface and Iface_3 with Type_Invariant'Class => Mark (Iface_4_Id); type Synch_1 is synchronized interface with Type_Invariant'Class => Mark (Synch_1_Id); type Synch_2 is synchronized interface and Synch_1 with Type_Invariant'Class => Mark (Synch_2_Id); ------------------ -- Tagged types -- ------------------ type Tag_1 is tagged private; type Tag_2 is tagged private; type Tag_3 is tagged private with Type_Invariant => Mark (Tag_3_Id); type Tag_4 is tagged private with Type_Invariant'Class => Mark (Tag_4_Id); -- Derivations without invariants type Tag_5 is new Tag_2 with private; type Tag_6 is new Tag_3 with private; type Tag_7 is new Tag_4 with private; -- Derivations with invariants on the full view type Tag_8 is new Tag_2 with private; type Tag_9 is new Tag_3 with private; type Tag_10 is new Tag_4 with private; -- Derivations with invariants type Tag_11 is new Tag_2 with private with Type_Invariant => Mark (Tag_11_Id); type Tag_12 is new Tag_3 with private with Type_Invariant => Mark (Tag_12_Id); type Tag_13 is new Tag_4 with private with Type_Invariant => Mark (Tag_13_Id); -- Derivations with class-wide invariants type Tag_14 is new Tag_2 with private with Type_Invariant'Class => Mark (Tag_14_Id); type Tag_15 is new Tag_3 with private with Type_Invariant'Class => Mark (Tag_15_Id); type Tag_16 is new Tag_4 with private with Type_Invariant'Class => Mark (Tag_16_Id); -- Derivations with interfaces type Tag_17 is new Tag_1 and Iface_1 and Iface_2 and Iface_3 and Iface_4 with private; type Tag_18 is new Tag_6 and Iface_1 and Iface_4 with private; type Tag_19 is new Tag_10 and Iface_2 and Iface_3 with private with Type_Invariant => Mark (Tag_19_Id); type Tag_20 is new Tag_11 and Iface_4 with private with Type_Invariant'Class => Mark (Tag_20_Id); -- Derivations with a hidden parent type Tag_21 is tagged private; type Tag_22 is tagged private; type Tag_23 is tagged private with Type_Invariant => Mark (Tag_23_Id); type Tag_24 is tagged private with Type_Invariant'Class => Mark (Tag_24_Id); -- Derivations with more derived parents type Tag_25 is new Tag_4 with private; type Tag_26 is new Tag_3 with private; type Tag_27 is new Tag_2 with private with Type_Invariant => Mark (Tag_27_Id); type Tag_28 is new Tag_4 with private with Type_Invariant'Class => Mark (Tag_28_Id); -- Parents of extensions type Par_1 (Discr_1 : Boolean) is tagged private; type Par_2 is tagged private; type Par_3 is tagged private with Type_Invariant => Mark (Par_3_Id); type Par_4 (Discr_1 : Boolean) is tagged private with Type_Invariant'Class => Mark (Par_4_Id); -- Extensions type Ext_1 is new Par_1 with private; type Ext_2 is new Par_1 with private with Type_Invariant => Mark (Ext_2_Id); type Ext_3 is new Par_2 with private; type Ext_4 is new Par_2 with private with Type_Invariant'Class => Mark (Ext_4_Id); type Ext_5 is new Par_3 with private with Type_Invariant => Mark (Ext_5_Id); type Ext_6 is new Par_3 with private; type Ext_7 is new Par_4 with private; type Ext_8 is new Par_4 with private with Type_Invariant => Mark (Ext_8_Id); -- Protected types type Prot_1 is limited private; type Prot_2 is limited private with Type_Invariant => Mark (Prot_2_Id); type Prot_3 is synchronized new Synch_2 with private with Type_Invariant'Class => Mark (Prot_3_Id); -- Task types type Task_1 is limited private with Type_Invariant => Mark (Task_1_Id); type Task_2 is synchronized new Synch_1 with private with Type_Invariant'Class => Mark (Task_2_Id); -------------------- -- Untagged types -- -------------------- type Untag_1 is private; type Untag_2 is private; type Untag_3 is private with Type_Invariant => Mark (Untag_3_Id); -- Composite types with invariants carrying invariants type Untag_4 is private; type Untag_5 is private; type Untag_6 is private; type Untag_7 is private; type Untag_8 (Discr : Boolean) is private; type Untag_9 (<>) is private; procedure Test_Deriv_1; procedure Test_Deriv_2; procedure Test_Deriv_3; procedure Test_Deriv_4; procedure Test_Deriv_5; procedure Test_Sub_1; procedure Test_Sub_2; procedure Test_Sub_3; procedure Test_Sub_4; procedure Test_Sub_5; procedure Test_Untag_9_TT; procedure Test_Untag_9_TF; procedure Test_Untag_9_FT; procedure Test_Untag_9_FF; private type Tag_1 is tagged null record; -- none type Tag_2 is tagged null record with Type_Invariant => Mark (Tag_2_Id); -- own: Tag_2_Id type Tag_3 is tagged null record; -- own: Tag_3_Id type Tag_4 is tagged null record with Type_Invariant => Mark (Tag_4_FV_Id); -- own: Tag_4_Id, Tag_4_FV_Id -- inheritable: Tag_4_Id type Tag_5 is new Tag_2 with null record; -- none type Tag_6 is new Tag_3 with null record; -- none type Tag_7 is new Tag_4 with null record; -- inherited: Tag_4_Id type Tag_8 is new Tag_2 with null record with Type_Invariant => Mark (Tag_8_Id); -- own: Tag_8_Id type Tag_9 is new Tag_3 with null record with Type_Invariant => Mark (Tag_9_Id); -- own: Tag_9_Id type Tag_10 is new Tag_4 with null record with Type_Invariant => Mark (Tag_10_Id); -- own: Tag_10_Id -- inherited: Tag_4_Id type Tag_11 is new Tag_2 with null record; -- own: Tag_11_Id type Tag_12 is new Tag_3 with null record; -- own: Tag_12_Id type Tag_13 is new Tag_4 with null record; -- own: Tag_13_Id -- inherited: Tag_4_Id type Tag_14 is new Tag_2 with null record; -- own: Tag_14_Id type Tag_15 is new Tag_3 with null record with Type_Invariant => Mark (Tag_15_FV_Id); -- own: Tag_15_Id, Tag_15_FV_Id type Tag_16 is new Tag_4 with null record; -- own: Tag_16_Id -- inheritable: Tag_16_Id -- inherited: Tag_4_Id type Tag_17 is new Tag_1 and Iface_1 and Iface_2 and Iface_3 and Iface_4 with null record; -- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id type Tag_18 is new Tag_6 and Iface_1 and Iface_4 with null record with Type_Invariant => Mark (Tag_18_Id); -- own: Tag_18_Id -- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id type Tag_19 is new Tag_10 and Iface_2 and Iface_3 with null record; -- own: Tag_19_Id -- inherited: Iface_1_Id, Iface_2_Id, Tag_4_Id type Tag_20 is new Tag_11 and Iface_4 with null record with Type_Invariant => Mark (Tag_20_FV_Id); -- own: Tag_20_Id, Tag_20_FV_Id -- inheritable: Tag_20_Id -- inherited : Iface_1_Id, Iface_2_Id, Iface_4_Id type Tag_21 is new Tag_15 with null record; -- inherited: Tag_15_Id type Tag_22 is new Tag_13 with null record with Type_Invariant => Mark (Tag_22_Id); -- own: Tag_22_Id -- inherited: Tag_4_Id type Tag_23 is new Tag_9 with null record; -- own: Tag_23_Id type Tag_24 is new Tag_15 with null record with Type_Invariant => Mark (Tag_24_FV_Id); -- own: Tag_24_Id, Tag_24_FV_Id -- inheritable: Tag_24_Id -- inherited: Tag_15_Id type Tag_25 is new Tag_13 with null record; -- inherited: Tag_4_Id type Tag_26 is new Tag_15 with null record with Type_Invariant => Mark (Tag_26_Id); -- own: Tag_26_Id -- inherited: Tag_15_Id type Tag_27 is new Tag_14 with null record; -- own: Tag_27_Id -- inherited: Tag_14_Id type Tag_28 is new Tag_13 with null record; -- own: Tag_28_Id -- inherited: Tag_4_Id type Par_1 (Discr_1 : Boolean) is tagged record Comp_1 : Tag_8; -- Tag_8_Id case Discr_1 is when True => Comp_2 : Tag_10; -- Tag_4_Id, Tag_10_Id when others => Comp_3 : Tag_19; -- Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id end case; end record; type Par_2 is tagged record Comp_1 : Tag_22; -- Tag_4_Id, Tag_22_Id Comp_2 : Tag_24; -- Tag_15_Id, Tag_24_Id, Tag_24_FV_Id end record with Type_Invariant => Mark (Par_2_FV_Id); -- own: Par_2_FV_Id -- calls: Tag_4_Id, Tag_15_Id, Tag_22_Id, Tag_24_Id, Tag_24_FV_Id type Par_3 is tagged record Comp_1 : Tag_1; -- none Comp_2 : Tag_6; -- none end record; -- own: Par_3_Id type Par_4 (Discr_1 : Boolean) is tagged record case Discr_1 is when True => Comp_1 : Tag_5; -- none when others => Comp_2 : Tag_6; -- none end case; end record with Type_Invariant => Mark (Par_4_FV_Id); -- own: Par_4_Id, Par_4_FV_Id -- inheritable: Par_4_Id type Ext_1 is new Par_1 with record Comp_4 : Tag_26; -- Tag_15_Id, Tag_26_Id Comp_5 : Tag_20; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_20_Id, -- Tag_20_FV_Id end record with Type_Invariant => Mark (Ext_1_FV_Id); -- calls: must be calculated -- own: Ext_1_FV_Id type Ext_2 is new Par_1 with record Comp_4 : Tag_1; -- none end record; -- calls: must be calculated -- own: Ext_2_Id type Ext_3 is new Par_2 with record Comp_3 : Tag_19; -- Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id end record; -- calls: Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_15_Id, Tag_19_Id, -- Tag_22_Id, Tag_24_Id, Tag_24_FV_Id type Ext_4 is new Par_2 with record Comp_3 : Tag_14; -- Tag_14_Id Comp_4 : Tag_25; -- Tag_4_Id end record with Type_Invariant => Mark (Ext_4_FV_Id); -- calls: Tag_4_Id, Tag_14_Id, Tag_15_Id, Tag_22_Id, Tag_24_Id, -- Tag_24_FV_Id -- own: Ext_4_Id, Ext_4_FV_Id -- inheritable: Ext_4_Id type Ext_5 is new Par_3 with record Comp_3 : Tag_18; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id end record; -- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id -- own: Ext_5_Id type Ext_6 is new Par_3 with record Comp_4 : Tag_4; -- Tag_4_Id, Tag_4_FV_Id end record with Type_Invariant => Mark (Ext_6_FV_Id); -- calls: Tag_4_Id, Tag_4_FV_Id -- own: Ext_6_FV_Id type Ext_7 is new Par_4 with record Comp_3 : Tag_6; -- none Comp_4 : Tag_28; -- Tag_4_Id, Tag_28_Id end record; -- calls: must be calculated type Ext_8 is new Par_4 with record Comp_3 : Tag_20; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_20_Id, -- Tag_20_FV_Id end record; -- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Par_4_Id, Tag_20_Id, -- Tag_20_FV_Id -- own: Ext_8_Id protected type Prot_1 with Type_Invariant => Mark (Prot_1_FV_Id) is entry E; private Comp_1 : Tag_18; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id end Prot_1; -- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id -- own: Prot_1_FV_Id protected type Prot_2 is entry E; private Comp_1 : Tag_5; -- none Comp_2 : Tag_21; -- Tag_15_Id end Prot_2; -- calls: Tag_15_Id -- own: Prot_2_Id protected type Prot_3 with Type_Invariant => Mark (Prot_3_FV_Id) is new Synch_2 with entry E; private Comp_1 : Tag_24; -- Tag_15_Id, Tag_24_Id, Tag_24_FV_Id end Prot_3; -- calls: Tag_15_Id, Tag_24_Id, Tag_24_FV_Id -- own: Prot_3_Id, Prot_3_FV_Id -- inheritable: Prot_3_Id -- inherited: Synch_1_Id, Synch_2_Id task type Task_1 is entry E; end Task_1; -- own: Task_1_Id task type Task_2 with Type_Invariant => Mark (Task_2_FV_Id) is new Synch_1 with entry E; end Task_2; -- own: Task_2_Id, Task_2_FV_Id -- inherited: Synch_1_Id type Untag_1 is new Integer; -- none type Untag_2 is record Comp : Integer; end record with Type_Invariant => Mark (Untag_2_Id); -- own: Untag_2_Id type Untag_3 is array (1 .. 5) of Boolean; -- own: Untag_3_Id type Untag_4 is record Comp_1 : Tag_16; -- Tag_4_Id, Tag_16_Id Comp_2 : Tag_18; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id Comp_3 : Tag_26; -- Tag_15_Id, Tag_26_Id end record; -- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_15_Id, -- Tag_16_Id, Tag_18_Id, Tag_26_Id type Untag_5 is record Comp_1 : Tag_17; -- Iface_1_Id, Iface_2_Id, Iface_4_Id Comp_2 : Tag_19; -- Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id Comp_3 : Tag_27; -- Tag_14_Id, Tag_27_Id end record with Type_Invariant => Mark (Untag_5_Id); -- own: Untag_5_Id -- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_14_Id, -- Tag_19_Id, Tag_27_Id type Untag_6 is array (1 .. 3, 5 .. 9) of Tag_10; -- calls: Tag_4_Id, Tag_10_Id type Untag_7 is array (1 .. 3) of Tag_13 with Type_Invariant => Mark (Untag_7_Id); -- own: Untag_7_Id -- calls: Tag_4_Id, Tag_13_Id type Untag_8 (Discr : Boolean) is record Comp_1 : Tag_18; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id case Discr is when True => Comp_2 : Tag_1; -- none when others => Comp_3 : Untag_5; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, -- Tag_4_Id, Tag_14_Id, Tag_19_Id, Tag_27_Id, -- Untag_5_Id end case; end record; type Untag_9 (Discr_1 : Boolean; Discr_2 : Boolean) is record Comp_1 : Tag_22; -- Tag_4_Id, Tag_22_Id case Discr_1 is when True => Comp_2 : Tag_28; -- Tag_4_Id, Tag_28_Id case Discr_2 is when True => Comp_3 : Untag_1; -- none when others => Comp_4 : Tag_1; -- none end case; when others => Comp_5 : Tag_4; -- Tag_4_Id, Tag_4_FV_Id Comp_6 : Tag_24; -- Tag_15_Id, Tag_24_Id, Tag_24_FV_Id case Discr_2 is when True => Comp_7 : Tag_27; -- Tag_14_Id, Tag_27_Id when others => Comp_8 : Untag_4; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, -- Tag_4_Id, Tag_15_Id, Tag_16_Id, -- Tag_18_Id, Tag_26_Id end case; end case; end record with Type_Invariant => Mark (Untag_9_Id); -- own: Untag_9_Id ------------------- -- Derived types -- ------------------- type Deriv_1 is new Tag_4 with null record; -- inherited: Tag_4_Id type Deriv_2 is new Tag_16 with null record; -- inherited: Tag_4_Id, Tag_16_Id type Deriv_3 is new Tag_18 with null record; -- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id type Deriv_4 is new Untag_4; -- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_15_Id, -- Tag_16_Id, Tag_18_Id, Tag_26_Id type Deriv_5 is new Untag_7; -- inherited: Tag_4_Id, Tag_13_Id, Untag_7_Id -------------- -- Subtypes -- -------------- subtype Sub_1 is Tag_9; -- inherited: Tag_9_Id subtype Sub_2 is Tag_17; -- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id subtype Sub_3 is Untag_2; -- inherited: Untag_2_Id subtype Sub_4 is Untag_5; -- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_14_Id, -- Tag_19_Id, Tag_27_Id, Untag_5_Id subtype Sub_5 is Untag_6; -- inherited: Tag_4_Id, Tag_10_Id end Invariants_Aspects; -- invariants_aspects.adb package body Invariants_Aspects is protected body Prot_1 is entry E when True is begin null; end E; end Prot_1; protected body Prot_2 is entry E when True is begin null; end E; end Prot_2; protected body Prot_3 is entry E when True is begin null; end E; end Prot_3; task body Task_1 is begin select accept E do null; end E; or terminate; end select; end Task_1; task body Task_2 is begin select accept E do null; end E; or terminate; end select; end Task_2; procedure Test_Deriv_1 is begin Reset_Results; declare Obj : Deriv_1; begin Test_Results ("Deriv_1", (Tag_4_Id => True, others => False)); end; end Test_Deriv_1; procedure Test_Deriv_2 is begin Reset_Results; declare Obj : Deriv_2; begin Test_Results ("Deriv_2", (Tag_4_Id => True, Tag_16_Id => True, others => False)); end; end Test_Deriv_2; procedure Test_Deriv_3 is begin Reset_Results; declare Obj : Deriv_3; begin Test_Results ("Deriv_3", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, others => False)); end; end Test_Deriv_3; procedure Test_Deriv_4 is begin Reset_Results; declare Obj : Deriv_4; begin Test_Results ("Deriv_4", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_4_Id => True, Tag_15_Id => True, Tag_16_Id => True, Tag_18_Id => True, Tag_26_Id => True, others => False)); end; end Test_Deriv_4; procedure Test_Deriv_5 is begin Reset_Results; declare Obj : Deriv_5; begin Test_Results ("Deriv_5", (Tag_4_Id => True, Tag_13_Id => True, others => False)); end; end Test_Deriv_5; procedure Test_Sub_1 is begin Reset_Results; declare Obj : Sub_1; begin Test_Results ("Sub_1", (Tag_9_Id => True, others => False)); end; end Test_Sub_1; procedure Test_Sub_2 is begin Reset_Results; declare Obj : Sub_2; begin Test_Results ("Sub_2", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, others => False)); end; end Test_Sub_2; procedure Test_Sub_3 is begin Reset_Results; declare Obj : Sub_3; begin Test_Results ("Sub_3", (Untag_2_Id => True, others => False)); end; end Test_Sub_3; procedure Test_Sub_4 is begin Reset_Results; declare Obj : Sub_4; begin Test_Results ("Sub_4", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_4_Id => True, Tag_14_Id => True, Tag_19_Id => True, Tag_27_Id => True, Untag_5_Id => True, others => False)); end; end Test_Sub_4; procedure Test_Sub_5 is begin Reset_Results; declare Obj : Sub_5; begin Test_Results ("Sub_5", (Tag_4_Id => True, Tag_10_Id => True, others => False)); end; end Test_Sub_5; procedure Test_Untag_9_TT is begin Reset_Results; declare Obj : Untag_9 (True, True); begin Test_Results ("Untag_9_TT", (Tag_4_Id => True, Tag_22_Id => True, Tag_28_Id => True, Untag_9_Id => True, others => False)); end; end Test_Untag_9_TT; procedure Test_Untag_9_TF is begin Reset_Results; declare Obj : Untag_9 (True, False); begin Test_Results ("Untag_9_TF", (Tag_4_Id => True, Tag_22_Id => True, Tag_28_Id => True, Untag_9_Id => True, others => False)); end; end Test_Untag_9_TF; procedure Test_Untag_9_FT is begin Reset_Results; declare Obj : Untag_9 (False, True); begin Test_Results ("Untag_9_FT", (Tag_4_Id => True, Tag_4_FV_Id => True, Tag_14_Id => True, Tag_15_Id => True, Tag_22_Id => True, Tag_24_Id => True, Tag_24_FV_Id => True, Tag_27_Id => True, Untag_9_Id => True, others => False)); end; end Test_Untag_9_FT; procedure Test_Untag_9_FF is begin Reset_Results; declare Obj : Untag_9 (False, False); begin Test_Results ("Untag_9_FF", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_4_Id => True, Tag_4_FV_Id => True, Tag_15_Id => True, Tag_16_Id => True, Tag_18_Id => True, Tag_22_Id => True, Tag_24_Id => True, Tag_24_FV_Id => True, Tag_26_Id => True, Untag_9_Id => True, others => False)); end; end Test_Untag_9_FF; end Invariants_Aspects; -- invariants_main.adb with Invariants_Aspects; use Invariants_Aspects; with Tester; use Tester; procedure Invariants_Main is begin Reset_Results; declare Obj : Tag_1; begin Test_Results ("Tag_1", (others => False)); end; Reset_Results; declare Obj : Tag_2; begin Test_Results ("Tag_2", (Tag_2_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_3; begin Test_Results ("Tag_3", (Tag_3_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_4; begin Test_Results ("Tag_4", (Tag_4_Id => True, Tag_4_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_5; begin Test_Results ("Tag_5", (others => False)); end; Reset_Results; declare Obj : Tag_6; begin Test_Results ("Tag_6", (others => False)); end; Reset_Results; declare Obj : Tag_7; begin Test_Results ("Tag_7", (Tag_4_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_8; begin Test_Results ("Tag_8", (Tag_8_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_9; begin Test_Results ("Tag_9", (Tag_9_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_10; begin Test_Results ("Tag_10", (Tag_4_Id => True, Tag_10_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_11; begin Test_Results ("Tag_11", (Tag_11_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_12; begin Test_Results ("Tag_12", (Tag_12_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_13; begin Test_Results ("Tag_13", (Tag_4_Id => True, Tag_13_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_14; begin Test_Results ("Tag_14", (Tag_14_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_15; begin Test_Results ("Tag_15", (Tag_15_Id => True, Tag_15_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_16; begin Test_Results ("Tag_16", (Tag_4_Id => True, Tag_16_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_17; begin Test_Results ("Tag_17", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_18; begin Test_Results ("Tag_18", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_18_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_19; begin Test_Results ("Tag_19", (Iface_1_Id => True, Iface_2_Id => True, Tag_4_Id => True, Tag_19_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_20; begin Test_Results ("Tag_20", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_20_Id => True, Tag_20_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_21; begin Test_Results ("Tag_21", (Tag_15_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_22; begin Test_Results ("Tag_22", (Tag_4_Id => True, Tag_22_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_23; begin Test_Results ("Tag_23", (Tag_23_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_24; begin Test_Results ("Tag_24", (Tag_15_Id => True, Tag_24_Id => True, Tag_24_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_25; begin Test_Results ("Tag_25", (Tag_4_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_26; begin Test_Results ("Tag_26", (Tag_15_Id => True, Tag_26_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_27; begin Test_Results ("Tag_27", (Tag_14_Id => True, Tag_27_Id => True, others => False)); end; Reset_Results; declare Obj : Tag_28; begin Test_Results ("Tag_28", (Tag_4_Id => True, Tag_28_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_1 (True); begin Test_Results ("Ext_1_T", (Ext_1_FV_Id => True, Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_4_Id => True, Tag_8_Id => True, Tag_10_Id => True, Tag_15_Id => True, Tag_20_Id => True, Tag_20_FV_Id => True, Tag_26_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_1 (False); begin Test_Results ("Ext_1_F", (Ext_1_FV_Id => True, Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_4_Id => True, Tag_8_Id => True, Tag_15_Id => True, Tag_19_Id => True, Tag_20_Id => True, Tag_20_FV_Id => True, Tag_26_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_2 (True); begin Test_Results ("Ext_2_T", (Ext_2_Id => True, Tag_4_Id => True, Tag_8_Id => True, Tag_10_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_2 (False); begin Test_Results ("Ext_2_F", (Ext_2_Id => True, Iface_1_Id => True, Iface_2_Id => True, Tag_4_Id => True, Tag_8_Id => True, Tag_19_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_3; begin Test_Results ("Ext_3", (Iface_1_Id => True, Iface_2_Id => True, Tag_4_Id => True, Tag_15_Id => True, Tag_19_Id => True, Tag_22_Id => True, Tag_24_Id => True, Tag_24_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_4; begin Test_Results ("Ext_4", (Ext_4_Id => True, Ext_4_FV_Id => True, Tag_4_Id => True, Tag_14_Id => True, Tag_15_Id => True, Tag_22_Id => True, Tag_24_Id => True, Tag_24_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_5; begin Test_Results ("Ext_5", (Ext_5_Id => True, Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_18_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_6; begin Test_Results ("Ext_6", (Ext_6_FV_Id => True, Tag_4_Id => True, Tag_4_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_7 (True); begin Test_Results ("Ext_7_T", (Par_4_Id => True, Tag_4_Id => True, Tag_28_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_7 (False); begin Test_Results ("Ext_7_F", (Par_4_Id => True, Tag_4_Id => True, Tag_28_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_8 (True); begin Test_Results ("Ext_8_T", (Ext_8_Id => True, Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Par_4_Id => True, Tag_20_Id => True, Tag_20_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Ext_8 (False); begin Test_Results ("Ext_8_F", (Ext_8_Id => True, Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Par_4_Id => True, Tag_20_Id => True, Tag_20_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Prot_1; begin Test_Results ("Prot_1", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Prot_1_FV_Id => True, Tag_18_Id => True, others => False)); end; Reset_Results; declare Obj : Prot_2; begin Test_Results ("Prot_2", (Prot_2_Id => True, Tag_15_Id => True, others => False)); end; Reset_Results; declare Obj : Prot_3; begin Test_Results ("Prot_3", (Prot_3_Id => True, Prot_3_FV_Id => True, Synch_1_Id => True, Synch_2_Id => True, Tag_15_Id => True, Tag_24_Id => True, Tag_24_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Task_1; begin Test_Results ("Task_1", (Task_1_Id => True, others => False)); end; Reset_Results; declare Obj : Task_2; begin Test_Results ("Task_2", (Synch_1_Id => True, Task_2_Id => True, Task_2_FV_Id => True, others => False)); end; Reset_Results; declare Obj : Untag_1; begin Test_Results ("Untag_1", (others => False)); end; Reset_Results; declare Obj : Untag_2; begin Test_Results ("Untag_2", (Untag_2_Id => True, others => False)); end; Reset_Results; declare Obj : Untag_3; begin Test_Results ("Untag_3", (Untag_3_Id => True, others => False)); end; Reset_Results; declare Obj : Untag_4; begin Test_Results ("Untag_4", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_4_Id => True, Tag_15_Id => True, Tag_16_Id => True, Tag_18_Id => True, Tag_26_Id => True, others => False)); end; Reset_Results; declare Obj : Untag_5; begin Test_Results ("Untag_5", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_4_Id => True, Tag_14_Id => True, Tag_19_Id => True, Tag_27_Id => True, Untag_5_Id => True, others => False)); end; Reset_Results; declare Obj : Untag_6; begin Test_Results ("Untag_6", (Tag_4_Id => True, Tag_10_Id => True, others => False)); end; Reset_Results; declare Obj : Untag_7; begin Test_Results ("Untag_7", (Tag_4_Id => True, Tag_13_Id => True, Untag_7_Id => True, others => False)); end; Reset_Results; declare Obj : Untag_8 (True); begin Test_Results ("Untag_8_T", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_18_Id => True, others => False)); end; Reset_Results; declare Obj : Untag_8 (False); begin Test_Results ("Untag_8_F", (Iface_1_Id => True, Iface_2_Id => True, Iface_4_Id => True, Tag_4_Id => True, Tag_14_Id => True, Tag_18_Id => True, Tag_19_Id => True, Tag_27_Id => True, Untag_5_Id => True, others => False)); end; Test_Untag_9_TT; Test_Untag_9_TF; Test_Untag_9_FT; Test_Untag_9_FF; Test_Deriv_1; Test_Deriv_2; Test_Deriv_3; Test_Deriv_4; Test_Deriv_5; Test_Sub_1; Test_Sub_2; Test_Sub_3; Test_Sub_4; Test_Sub_5; end Invariants_Main; ---------------------------- -- Compilation and output -- ---------------------------- $ gnatmake -q -gnata -gnatws invariants_main.adb $ ./invariants_main Tag_1: OK Tag_2: OK Tag_3: OK Tag_4: OK Tag_5: OK Tag_6: OK Tag_7: OK Tag_8: OK Tag_9: OK Tag_10: OK Tag_11: OK Tag_12: OK Tag_13: OK Tag_14: OK Tag_15: OK Tag_16: OK Tag_17: OK Tag_18: OK Tag_19: OK Tag_20: OK Tag_21: OK Tag_22: OK Tag_23: OK Tag_24: OK Tag_25: OK Tag_26: OK Tag_27: OK Tag_28: OK Ext_1_T: OK Ext_1_F: OK Ext_2_T: OK Ext_2_F: OK Ext_3: OK Ext_4: OK Ext_5: OK Ext_6: OK Ext_7_T: OK Ext_7_F: OK Ext_8_T: OK Ext_8_F: OK Prot_1: OK Prot_2: OK Prot_3: OK Task_1: OK Task_2: OK Untag_1: OK Untag_2: OK Untag_3: OK Untag_4: OK Untag_5: OK Untag_6: OK Untag_7: OK Untag_8_T: OK Untag_8_F: OK Untag_9_TT: OK Untag_9_TF: OK Untag_9_FT: OK Untag_9_FF: OK Deriv_1: OK Deriv_2: OK Deriv_3: OK Deriv_4: OK Deriv_5: OK Sub_1: OK Sub_2: OK Sub_3: OK Sub_4: OK Sub_5: OK Tested on x86_64-pc-linux-gnu, committed on trunk 2016-06-16 Hristian Kirtchev <kirtchev@adacore.com> * atree.ads, atree.adb (Elist29): New routine. (Set_Elist29): New routine. * atree.h New definition for Elist29. * einfo.adb Subprograms_For_Type is now an Elist rather than a node. Has_Invariants is now a synthesized attribute and does not require a flag. Has_Own_Invariants is now Flag232. Has_Inherited_Invariants is Flag291. Is_Partial_Invariant_Procedure is Flag292. (Default_Init_Cond_Procedure): Reimplemented. (Has_Inherited_Invariants): New routine. (Has_Invariants): Reimplemented. (Has_Own_Invariants): New routine. (Invariant_Procedure): Reimplemented. (Is_Partial_Invariant_Procedure): New routine. (Partial_Invariant_Procedure): Reimplemented. (Predicate_Function): Reimplemented. (Predicate_Function_M): Reimplemented. (Set_Default_Init_Cond_Procedure): Reimplemented. (Set_Has_Inherited_Invariants): New routine. (Set_Has_Invariants): Removed. (Set_Has_Own_Invariants): New routine. (Set_Invariant_Procedure): Reimplemented. (Set_Is_Partial_Invariant_Procedure): New routine. (Set_Partial_Invariant_Procedure): Reimplemented. (Set_Predicate_Function): Reimplemented. (Set_Predicate_Function_M): Reimplemented. (Set_Subprograms_For_Type): Reimplemented. (Subprograms_For_Type): Reimplemented. (Write_Entity_Flags): Output Flag232 and Flag291. * einfo.ads Add new attributes Has_Inherited_Invariants Has_Own_Invariants Is_Partial_Invariant_Procedure Partial_Invariant_Procedure Change the documentation of attributes Has_Inheritable_Invariants Has_Invariants Invariant_Procedure Is_Invariant_Procedure Subprograms_For_Type (Has_Inherited_Invariants): New routine along with pragma Inline. (Has_Own_Invariants): New routine along with pragma Inline. (Is_Partial_Invariant_Procedure): New routine along with pragma Inline. (Partial_Invariant_Procedure): New routine. (Set_Has_Inherited_Invariants): New routine along with pragma Inline. (Set_Has_Invariants): Removed along with pragma Inline. (Set_Has_Own_Invariants): New routine along with pragma Inline. (Set_Is_Partial_Invariant_Procedure): New routine along with pragma Inline. (Set_Partial_Invariant_Procedure): New routine. (Set_Subprograms_For_Type): Update the signature. (Subprograms_For_Type): Update the signature. * exp_ch3.adb Remove with and use clauses for Sem_Ch13. (Build_Array_Invariant_Proc): Removed. (Build_Record_Invariant_Proc): Removed. (Freeze_Type): Build the body of the invariant procedure. (Insert_Component_Invariant_Checks): Removed. * exp_ch7.adb Add with and use clauses for Sem_Ch6, Sem_Ch13, and Stringt. (Build_Invariant_Procedure_Body): New routine. (Build_Invariant_Procedure_Declaration): New routine. * exp_ch7.ads (Build_Invariant_Procedure_Body): New routine. (Build_Invariant_Procedure_Declaration): New routine. * exp_ch9.adb (Build_Corresponding_Record): Do not propagate attributes related to invariants to the corresponding record when building the corresponding record. This is done by Build_Invariant_Procedure_Declaration. * exp_util.adb (Make_Invariant_Call): Reimplemented. * freeze.adb (Freeze_Array_Type): An array type requires an invariant procedure when its component type has invariants. (Freeze_Record_Type): A record type requires an invariant procedure when at least one of its components has an invariant. * sem_ch3.adb (Analyze_Private_Extension_Declaration): Inherit invariant-related attributes. (Analyze_Subtype_Declaration): Inherit invariant-related attributes. (Build_Derived_Record_Type): Inherit invariant-related attributes. (Check_Duplicate_Aspects): Reimplemented. (Get_Partial_View_Aspect): New routine. (Process_Full_View): Inherit invariant-related attributes. Reimplement the check on hidden inheritance of class-wide invariants. (Remove_Default_Init_Cond_Procedure): Reimplemented. * sem_ch6.adb (Analyze_Subprogram_Specification): Do not modify the controlling type for an invariant procedure declaration or body. (Is_Invariant_Procedure_Or_Body): New routine. * sem_ch7.adb (Analyze_Package_Specification): Build the partial invariant body in order to preanalyze and resolve all invariants of a private type at the end of the visible declarations. Build the full invariant body in order to preanalyze and resolve all invariants of a private type's full view at the end of the private declarations. (Preserve_Full_Attributes): Inherit invariant-related attributes. * sem_ch9.adb (Analyze_Protected_Type_Declaration): Ensure that aspects are analyzed with the proper view when the protected type is a completion of a private type. Inherit invariant-related attributes. (Analyze_Task_Type_Declaration): Ensure that aspects are analyzed with the proper view when the task type is a completion of a private type. Inherit invariant-related attributes. * sem_ch13.adb Remove with and use clauses for Stringt. (Build_Invariant_Procedure_Declaration): Removed. (Build_Invariant_Procedure): Removed. (Freeze_Entity_Checks): Do not build the body of the invariant procedure here. The body is built when the type is frozen in Freeze_Type. (Inherit_Aspects_At_Freeze_Point): Do not inherit any attributes related to invariants here because this leads to erroneous inheritance. (Replace_Node): Rename to Replace_Type_Ref. * sem_ch13.ads (Build_Invariant_Procedure_Declaration): Removed. (Build_Invariant_Procedure): Removed. * sem_prag.adb Add with and use clauses for Exp_Ch7. (Analyze_Pragma): Reimplement the analysis of pragma Invariant. * sem_res.adb (Resolve_Actuals): Emit a specialized error when the context is an invariant. * sem_util.adb (Get_Views): New routine. (Incomplete_Or_Partial_View): Consider generic packages when examining declarations. (Inspect_Decls): Consider full type declarations because they may denote a derivation from a private type. (Propagate_Invariant_Attributes): New routine. * sem_util.ads (Get_Views): New routine. (Propagate_Invariant_Attributes): New routine.