===================================================================
@@ -2279,12 +2279,32 @@
if Nkind (Context) = N_Package_Specification then
+ -- Preanalyze and resolve the class-wide invariants of an
+ -- interface at the end of whichever declarative part has the
+ -- interface type. Note that an interface may be declared in
+ -- any non-package declarative part, but reaching the end of
+ -- such a declarative part will always freeze the type and
+ -- generate the invariant procedure (see Freeze_Type).
+
+ if Is_Interface (Typ) then
+
+ -- Interfaces are treated as the partial view of a private
+ -- type in order to achieve uniformity with the general
+ -- case. As a result, an interface receives only a "partial"
+ -- invariant procedure which is never called.
+
+ if Has_Own_Invariants (Typ) then
+ Build_Invariant_Procedure_Body
+ (Typ => Typ,
+ Partial_Invariant => True);
+ end if;
+
-- Preanalyze and resolve the invariants of a private type
-- at the end of the visible declarations to catch potential
-- errors. Inherited class-wide invariants are not included
-- because they have already been resolved.
- if Decls = Visible_Declarations (Context)
+ elsif Decls = Visible_Declarations (Context)
and then Ekind_In (Typ, E_Limited_Private_Type,
E_Private_Type,
E_Record_Type_With_Private)
@@ -15315,10 +15335,9 @@
New_Overloaded_Entity (New_Subp, Derived_Type);
- -- Implement rule in 6.1.1 (15) : if subprogram inherits non-conforming
- -- classwide preconditions and the derived type is abstract, the
- -- derived operation is abstract as well if parent subprogram is not
- -- abstract or null.
+ -- Ada RM 6.1.1 (15): If a subprogram inherits non-conforming class-wide
+ -- preconditions and the derived type is abstract, the derived operation
+ -- is abstract as well if parent subprogram is not abstract or null.
if Is_Abstract_Type (Derived_Type)
and then Has_Non_Trivial_Precondition (Parent_Subp)
===================================================================
@@ -1989,7 +1989,7 @@
-- 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.
+ -- the body of the invariant procedure free of useless code.
procedure Add_Array_Component_Invariants
(T : Entity_Id;
@@ -2000,14 +2000,16 @@
-- invariant procedure. All created checks are added to list Checks.
procedure Add_Inherited_Invariants
- (Full_Typ : Entity_Id;
- Priv_Typ : Entity_Id;
- Obj_Id : Entity_Id;
- Checks : in out List_Id);
+ (T : Entity_Id;
+ Priv_Typ : Entity_Id;
+ Full_Typ : 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.
+ -- coming from all parent types of type T. Priv_Typ and Full_Typ denote
+ -- the partial and full view of the parent type. 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;
@@ -2196,7 +2198,6 @@
Attribute_Name => Name_Range,
Expressions => New_List (
Make_Integer_Literal (Loc, Dim))))),
-
Statements => Comp_Checks));
end if;
end if;
@@ -2216,25 +2217,36 @@
------------------------------
procedure Add_Inherited_Invariants
- (Full_Typ : Entity_Id;
- Priv_Typ : Entity_Id;
- Obj_Id : Entity_Id;
- Checks : in out List_Id)
+ (T : Entity_Id;
+ Priv_Typ : Entity_Id;
+ Full_Typ : Entity_Id;
+ Obj_Id : Entity_Id;
+ Checks : in out List_Id)
is
- Arg1 : Node_Id;
- Arg2 : Node_Id;
- Expr : Node_Id;
- Prag : Node_Id;
+ Deriv_Typ : Entity_Id;
+ Expr : Node_Id;
+ Prag : Node_Id;
+ Prag_Expr : Node_Id;
+ Prag_Expr_Arg : Node_Id;
+ Prag_Typ : Node_Id;
+ Prag_Typ_Arg : Node_Id;
- Rep_Typ : Entity_Id;
- -- The replacement type used in the substitution of the current
- -- instance of a type with the _object formal parameter
+ Par_Proc : Entity_Id;
+ -- The "partial" invariant procedure of Par_Typ
+ Par_Typ : Entity_Id;
+ -- The suitable view of the parent type used in the substitution of
+ -- type attributes.
+
begin
if not Present (Priv_Typ) and then not Present (Full_Typ) then
return;
end if;
+ -- Determine which rep item chain to use. Precedence is given to that
+ -- of the parent type's partial view since it usually carries all the
+ -- class-wide invariants.
+
if Present (Priv_Typ) then
Prag := First_Rep_Item (Priv_Typ);
else
@@ -2249,49 +2261,89 @@
if Contains (Pragmas_Seen, Prag) then
return;
+
+ -- Nothing to do when the caller requests the processing of all
+ -- inherited class-wide invariants, but the pragma does not
+ -- fall in this category.
+
+ elsif not Class_Present (Prag) then
+ return;
end if;
-- Extract the arguments of the invariant pragma
- Arg1 := First (Pragma_Argument_Associations (Prag));
- Arg2 := Get_Pragma_Arg (Next (Arg1));
- Arg1 := Get_Pragma_Arg (Arg1);
+ Prag_Typ_Arg := First (Pragma_Argument_Associations (Prag));
+ Prag_Expr_Arg := Next (Prag_Typ_Arg);
+ Prag_Expr := Expression_Copy (Prag_Expr_Arg);
+ Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg);
- -- The pragma applies to the partial view
+ -- The pragma applies to the partial view of the parent type
- if Present (Priv_Typ) and then Entity (Arg1) = Priv_Typ then
- Rep_Typ := Priv_Typ;
+ if Present (Priv_Typ)
+ and then Entity (Prag_Typ) = Priv_Typ
+ then
+ Par_Typ := Priv_Typ;
- -- The pragma applies to the full view
+ -- The pragma applies to the full view of the parent type
- elsif Present (Full_Typ) and then Entity (Arg1) = Full_Typ then
- Rep_Typ := Full_Typ;
+ elsif Present (Full_Typ)
+ and then Entity (Prag_Typ) = Full_Typ
+ then
+ Par_Typ := Full_Typ;
- -- Otherwise the pragma applies to a parent type and will be
- -- processed at a later step by routine Add_Parent_Invariants
- -- or Add_Interface_Invariants.
+ -- Otherwise the pragma does not belong to the parent type and
+ -- should not be considered.
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.
+ -- Perform the following substitutions:
- if not Class_Present (Prag) then
- return;
+ -- * Replace a reference to the _object parameter of the
+ -- parent type's partial invariant procedure with a
+ -- reference to the _object parameter of the derived
+ -- type's full invariant procedure.
+
+ -- * Replace a reference to a discriminant of the parent type
+ -- with a suitable value from the point of view of the
+ -- derived type.
+
+ -- * Replace a call to an overridden parent primitive with a
+ -- call to the overriding derived type primitive.
+
+ -- * Replace a call to an inherited parent primitive with a
+ -- call to the internally-generated inherited derived type
+ -- primitive.
+
+ Expr := New_Copy_Tree (Prag_Expr);
+
+ -- When the type inheriting the class-wide invariant is a task
+ -- or protected type, use the corresponding record type because
+ -- it contains all primitive operations of the concurren type
+ -- and allows for proper substitution.
+
+ if Is_Concurrent_Type (T) then
+ Deriv_Typ := Corresponding_Record_Type (T);
+ else
+ Deriv_Typ := T;
end if;
- Expr := New_Copy_Tree (Arg2);
+ pragma Assert (Present (Deriv_Typ));
- -- Substitute all references to type T with references to the
- -- _object formal parameter.
+ -- The parent type must have a "partial" invariant procedure
+ -- because class-wide invariants are captured exclusively by
+ -- it.
- -- ??? Dispatching must be removed due to AI12-0150-1
+ Par_Proc := Partial_Invariant_Procedure (Par_Typ);
+ pragma Assert (Present (Par_Proc));
- Replace_Type_References
- (Expr, Rep_Typ, Obj_Id, Dispatch => Class_Present (Prag));
+ Replace_References
+ (Expr => Expr,
+ Par_Typ => Par_Typ,
+ Deriv_Typ => Deriv_Typ,
+ Par_Obj => First_Formal (Par_Proc),
+ Deriv_Obj => Obj_Id);
Add_Invariant_Check (Prag, Expr, Checks, Inherited => True);
end if;
@@ -2323,11 +2375,17 @@
Iface_Elmt := First_Elmt (Ifaces);
while Present (Iface_Elmt) loop
+
+ -- The Full_Typ parameter is intentionally left Empty because
+ -- interfaces are treated as the partial view of a private type
+ -- in order to achieve uniformity with the general case.
+
Add_Inherited_Invariants
- (Full_Typ => Node (Iface_Elmt),
- Priv_Typ => Empty,
- Obj_Id => Obj_Id,
- Checks => Checks);
+ (T => T,
+ Priv_Typ => Node (Iface_Elmt),
+ Full_Typ => Empty,
+ Obj_Id => Obj_Id,
+ Checks => Checks);
Next_Elmt (Iface_Elmt);
end loop;
@@ -2358,7 +2416,7 @@
if Is_Ignored (Prag) then
null;
- -- Otherwise the invariant is checked. Build a Check pragma to verify
+ -- Otherwise the invariant is checked. Build a pragma Check to verify
-- the expression at runtime.
else
@@ -2479,10 +2537,11 @@
end if;
Add_Inherited_Invariants
- (Full_Typ => Full_Typ,
- Priv_Typ => Priv_Typ,
- Obj_Id => Obj_Id,
- Checks => Checks);
+ (T => T,
+ Priv_Typ => Priv_Typ,
+ Full_Typ => Full_Typ,
+ Obj_Id => Obj_Id,
+ Checks => Checks);
Curr_Typ := Par_Typ;
end loop;
@@ -2498,13 +2557,14 @@
Checks : in out List_Id;
Priv_Item : Node_Id := Empty)
is
- Arg1 : Node_Id;
- Arg2 : Node_Id;
- ASIS_Expr : Node_Id;
- Asp : Node_Id;
- Expr : Node_Id;
- Ploc : Source_Ptr;
- Prag : Node_Id;
+ ASIS_Expr : Node_Id;
+ Expr : Node_Id;
+ Prag : Node_Id;
+ Prag_Asp : Node_Id;
+ Prag_Expr : Node_Id;
+ Prag_Expr_Arg : Node_Id;
+ Prag_Typ : Node_Id;
+ Prag_Typ_Arg : Node_Id;
begin
if not Present (T) then
@@ -2531,49 +2591,49 @@
-- Extract the arguments of the invariant pragma
- Arg1 := First (Pragma_Argument_Associations (Prag));
- Arg2 := Get_Pragma_Arg (Next (Arg1));
- Arg1 := Get_Pragma_Arg (Arg1);
- Asp := Corresponding_Aspect (Prag);
- Ploc := Sloc (Prag);
+ Prag_Typ_Arg := First (Pragma_Argument_Associations (Prag));
+ Prag_Expr_Arg := Next (Prag_Typ_Arg);
+ Prag_Expr := Get_Pragma_Arg (Prag_Expr_Arg);
+ Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg);
+ Prag_Asp := Corresponding_Aspect (Prag);
-- Verify the pragma belongs to T, otherwise the pragma applies
-- to a parent type in which case it will be processed later by
-- Add_Parent_Invariants or Add_Interface_Invariants.
- if Entity (Arg1) /= T then
+ if Entity (Prag_Typ) /= T then
return;
end if;
- Expr := New_Copy_Tree (Arg2);
+ Expr := New_Copy_Tree (Prag_Expr);
-- Substitute all references to type T with references to the
-- _object formal parameter.
- Replace_Type_References
- (Expr => Expr,
- Typ => T,
- Obj_Id => Obj_Id,
- Dispatch => Class_Present (Prag));
+ Replace_Type_References (Expr, T, Obj_Id);
-- 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));
+ Set_Parent (Expr, Parent (Prag_Expr));
Preanalyze_Assert_Expression (Expr, Any_Boolean);
+ -- Save a copy of the expression when T is tagged to detect
+ -- errors and capture the visibility of the proper package part
+ -- for the generation of inherited type invariants.
+
+ if Is_Tagged_Type (T) then
+ Set_Expression_Copy (Prag_Expr_Arg, New_Copy_Tree (Expr));
+ end if;
+
-- 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));
+ if Present (Prag_Asp) then
+ Set_Entity (Identifier (Prag_Asp), New_Copy_Tree (Expr));
end if;
-- Analyze the original invariant expression for ASIS
@@ -2582,43 +2642,17 @@
ASIS_Expr := Empty;
if Comes_From_Source (Prag) then
- ASIS_Expr := Arg2;
- elsif Present (Asp) then
- ASIS_Expr := Expression (Asp);
+ ASIS_Expr := Prag_Expr;
+ elsif Present (Prag_Asp) then
+ ASIS_Expr := Expression (Prag_Asp);
end if;
if Present (ASIS_Expr) then
- Replace_Type_References
- (Expr => ASIS_Expr,
- Typ => T,
- Obj_Id => Obj_Id,
- Dispatch => Class_Present (Prag));
-
+ Replace_Type_References (ASIS_Expr, T, Obj_Id);
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;
-
Add_Invariant_Check (Prag, Expr, Checks);
end if;
@@ -2863,25 +2897,25 @@
Proc_Id : Entity_Id;
Stmts : List_Id := No_List;
- CRec_Typ : Entity_Id;
+ CRec_Typ : Entity_Id := Empty;
-- The corresponding record type of Full_Typ
- Full_Proc : Entity_Id;
+ Full_Proc : Entity_Id := Empty;
-- The entity of the "full" invariant procedure
- Full_Typ : Entity_Id;
+ Full_Typ : Entity_Id := Empty;
-- The full view of the working type
- Obj_Id : Entity_Id;
+ Obj_Id : Entity_Id := Empty;
-- The _object formal parameter of the invariant procedure
- Part_Proc : Entity_Id;
+ Part_Proc : Entity_Id := Empty;
-- The entity of the "partial" invariant procedure
- Priv_Typ : Entity_Id;
+ Priv_Typ : Entity_Id := Empty;
-- The partial view of the working type
- Work_Typ : Entity_Id;
+ Work_Typ : Entity_Id := Empty;
-- The working type
-- Start of processing for Build_Invariant_Procedure_Body
@@ -2917,16 +2951,17 @@
pragma Assert (Has_Invariants (Work_Typ));
- -- Nothing to do for interface types as their class-wide invariants are
- -- inherited by implementing types.
+ -- Interfaces are treated as the partial view of a private type in order
+ -- to achieve uniformity with the general case.
if Is_Interface (Work_Typ) then
- goto Leave;
- end if;
+ Priv_Typ := Work_Typ;
- -- Obtain both views of the type
+ -- Otherwise obtain both views of the type
- Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ);
+ else
+ Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ);
+ end if;
-- The caller requests a body for the partial invariant procedure
@@ -2990,10 +3025,10 @@
goto Leave;
end if;
- -- Emulate the environment of the invariant procedure by installing
- -- its scope and formal parameters. Note that this is not needed, but
- -- having the scope of the invariant procedure installed helps with
- -- the detection of invariant-related errors.
+ -- Emulate the environment of the invariant procedure by installing its
+ -- scope and formal parameters. Note that this is not needed, but having
+ -- the scope installed helps with the detection of invariant-related
+ -- errors.
Push_Scope (Proc_Id);
Install_Formals (Proc_Id);
@@ -3084,17 +3119,6 @@
end if;
end if;
- -- Process the elements of an array type
-
- if Is_Array_Type (Full_Typ) then
- Add_Array_Component_Invariants (Full_Typ, Obj_Id, Stmts);
-
- -- Process the components of a record type
-
- elsif Ekind (Full_Typ) = E_Record_Type then
- Add_Record_Component_Invariants (Full_Typ, Obj_Id, Stmts);
- 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.
@@ -3111,7 +3135,19 @@
Checks => Stmts,
Priv_Item => Priv_Item);
- if Present (CRec_Typ) then
+ -- Process the elements of an array type
+
+ if Is_Array_Type (Full_Typ) then
+ Add_Array_Component_Invariants (Full_Typ, Obj_Id, Stmts);
+
+ -- Process the components of a record type
+
+ elsif Ekind (Full_Typ) = E_Record_Type then
+ Add_Record_Component_Invariants (Full_Typ, Obj_Id, Stmts);
+
+ -- Process the components of a corresponding record
+
+ elsif Present (CRec_Typ) then
Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Stmts);
end if;
@@ -3144,7 +3180,7 @@
end if;
-- Generate:
- -- procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>) is
+ -- procedure <Work_Typ>[Partial_]Invariant (_object : <Obj_Typ>) is
-- begin
-- <Stmts>
-- end <Work_Typ>[Partial_]Invariant;
@@ -3226,6 +3262,9 @@
Obj_Id : Entity_Id;
-- The _object formal parameter of the invariant procedure
+ Obj_Typ : Entity_Id;
+ -- The type of the _object formal parameter
+
Priv_Typ : Entity_Id;
-- The partial view of working type
@@ -3263,15 +3302,9 @@
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
- goto Leave;
-
-- Nothing to do if the type already has a "partial" invariant procedure
- elsif Partial_Invariant then
+ if Partial_Invariant then
if Present (Partial_Invariant_Procedure (Work_Typ)) then
goto Leave;
end if;
@@ -3352,16 +3385,41 @@
Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject);
+ -- When generating an invariant procedure declaration for an abstract
+ -- type (including interfaces), use the class-wide type as the _object
+ -- type. This has several desirable effects:
+
+ -- * The invariant procedure does not become a primitive of the type.
+ -- This eliminates the need to either special case the treatment of
+ -- invariant procedures, or to make it a predefined primitive and
+ -- force every derived type to potentially provide an empty body.
+
+ -- * The invariant procedure does not need to be declared as abstract.
+ -- This allows for a proper body which in turn avoids redundant
+ -- processing of the same invariants for types with multiple views.
+
+ -- * The class-wide type allows for calls to abstract primitives
+ -- within a non-abstract subprogram. The calls are treated as
+ -- dispatching and require additional processing when they are
+ -- remapped to call primitives of derived types. See routine
+ -- Replace_References for details.
+
+ if Is_Abstract_Type (Work_Typ) then
+ Obj_Typ := Class_Wide_Type (Work_Typ);
+ else
+ Obj_Typ := Work_Typ;
+ end if;
+
-- Perform minor decoration in case the declaration is not analyzed
Set_Ekind (Obj_Id, E_In_Parameter);
- Set_Etype (Obj_Id, Work_Typ);
+ Set_Etype (Obj_Id, Obj_Typ);
Set_Scope (Obj_Id, Proc_Id);
Set_First_Entity (Proc_Id, Obj_Id);
-- Generate:
- -- procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>);
+ -- procedure <Work_Typ>[Partial_]Invariant (_object : <Obj_Typ>);
Proc_Decl :=
Make_Subprogram_Declaration (Loc,
@@ -3371,8 +3429,7 @@
Parameter_Specifications => New_List (
Make_Parameter_Specification (Loc,
Defining_Identifier => Obj_Id,
- Parameter_Type =>
- New_Occurrence_Of (Work_Typ, Loc)))));
+ Parameter_Type => New_Occurrence_Of (Obj_Typ, Loc)))));
-- The declaration should not be inserted into the tree when the context
-- is ASIS or a generic unit because it is not part of the template.
@@ -11448,6 +11505,37 @@
-----------------
function Replace_Ref (Ref : Node_Id) return Traverse_Result is
+ procedure Remove_Controlling_Arguments (From_Arg : Node_Id);
+ -- Reset the Controlling_Argument of all function calls which
+ -- encapsulate node From_Arg.
+
+ ----------------------------------
+ -- Remove_Controlling_Arguments --
+ ----------------------------------
+
+ procedure Remove_Controlling_Arguments (From_Arg : Node_Id) is
+ Par : Node_Id;
+
+ begin
+ Par := From_Arg;
+ while Present (Par) loop
+ if Nkind (Par) = N_Function_Call
+ and then Present (Controlling_Argument (Par))
+ then
+ Set_Controlling_Argument (Par, Empty);
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+ end Remove_Controlling_Arguments;
+
+ -- Local variables
+
Context : constant Node_Id := Parent (Ref);
Loc : constant Source_Ptr := Sloc (Ref);
Ref_Id : Entity_Id;
@@ -11463,6 +11551,8 @@
Val : Node_Or_Entity_Id;
-- The corresponding value of Ref from the type map
+ -- Start of processing for Replace_Ref
+
begin
-- Assume that the input reference is to be replaced and that the
-- traversal should examine the children of the reference.
@@ -11529,7 +11619,7 @@
end if;
-- The reference mentions the _object parameter of the parent
- -- type's DIC procedure. Replace as follows:
+ -- type's DIC or type invariant procedure. Replace as follows:
-- _object -> _object
@@ -11539,6 +11629,23 @@
then
New_Ref := New_Occurrence_Of (Deriv_Obj, Loc);
+ -- The type of the _object parameter is class-wide when the
+ -- expression comes from an assertion pragma which applies to
+ -- an abstract parent type or an interface. The class-wide type
+ -- facilitates the preanalysis of the expression by treating
+ -- calls to abstract primitives which mention the current
+ -- instance of the type as dispatching. Once the calls are
+ -- remapped to invoke overriding or inherited primitives, the
+ -- calls no longer need to be dispatching. Examine all function
+ -- calls which encapsule the _object parameter and reset their
+ -- Controlling_Argument attribute.
+
+ if Is_Class_Wide_Type (Etype (Par_Obj))
+ and then Is_Abstract_Type (Root_Type (Etype (Par_Obj)))
+ then
+ Remove_Controlling_Arguments (Old_Ref);
+ end if;
+
-- The reference to _object acts as an actual parameter in a
-- subprogram call which may be invoking a primitive of the
-- parent type:
@@ -11659,10 +11766,9 @@
-----------------------------
procedure Replace_Type_References
- (Expr : Node_Id;
- Typ : Entity_Id;
- Obj_Id : Entity_Id;
- Dispatch : Boolean := False)
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Obj_Id : Entity_Id)
is
procedure Replace_Type_Ref (N : Node_Id);
-- Substitute a single reference of the current instance of type Typ
@@ -11673,9 +11779,6 @@
----------------------
procedure Replace_Type_Ref (N : Node_Id) is
- Nloc : constant Source_Ptr := Sloc (N);
- Ref : Node_Id;
-
begin
-- Decorate the reference to Typ even though it may be rewritten
-- further down. This is done for two reasons:
@@ -11698,33 +11801,9 @@
-- Perform the following substitution:
- -- Typ -> _object
+ -- Typ --> _object
- Ref := Make_Identifier (Sloc (N), Chars (Obj_Id));
- Set_Entity (Ref, Obj_Id);
- Set_Etype (Ref, Typ);
-
- -- When the pragma denotes a class-wide and the Dispatch flag is set
- -- perform the following substitution. Note: dispatching in this
- -- fashion is illegal Ada according to AI12-0150-1 because class-wide
- -- aspects like type invariants and default initial conditions be
- -- evaluated statically. Currently it is used only for class-wide
- -- type invariants, but this will be fixed.
-
- -- Rep_Typ --> Rep_Typ'Class (_object)
-
- if Dispatch then
- Ref :=
- Make_Type_Conversion (Nloc,
- Subtype_Mark =>
- Make_Attribute_Reference (Nloc,
- Prefix =>
- New_Occurrence_Of (Typ, Nloc),
- Attribute_Name => Name_Class),
- Expression => Ref);
- end if;
-
- Rewrite (N, Ref);
+ Rewrite (N, New_Occurrence_Of (Obj_Id, Sloc (N)));
Set_Comes_From_Source (N, True);
end Replace_Type_Ref;
===================================================================
@@ -1062,10 +1062,9 @@
-- the internally-generated inherited primitive of Deriv_Typ.
procedure Replace_Type_References
- (Expr : Node_Id;
- Typ : Entity_Id;
- Obj_Id : Entity_Id;
- Dispatch : Boolean := False);
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Obj_Id : Entity_Id);
-- Substitute all references of the current instance of type Typ with
-- references to formal parameter Obj_Id within expression Expr.
===================================================================
@@ -17113,10 +17113,14 @@
Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
-- Create the declaration of the invariant procedure which will
- -- verify the invariant at run-time. Note that interfaces do not
- -- carry such a declaration.
+ -- verify the invariant at run-time. Interfaces are treated as the
+ -- partial view of a private type in order to achieve uniformity
+ -- with the general case. As a result, an interface receives only
+ -- a "partial" invariant procedure which is never called.
- Build_Invariant_Procedure_Declaration (Typ);
+ Build_Invariant_Procedure_Declaration
+ (Typ => Typ,
+ Partial_Invariant => Is_Interface (Typ));
end Invariant;
----------------
===================================================================
@@ -7529,7 +7529,22 @@
-- class-wide invariants from parent types or interfaces, and invariants
-- on array elements or record components.
- if Has_Invariants (Def_Id) then
+ if Is_Interface (Def_Id) then
+
+ -- Interfaces are treated as the partial view of a private type in
+ -- order to achieve uniformity with the general case. As a result, an
+ -- interface receives only a "partial" invariant procedure which is
+ -- never called.
+
+ if Has_Own_Invariants (Def_Id) then
+ Build_Invariant_Procedure_Body
+ (Typ => Def_Id,
+ Partial_Invariant => Is_Interface (Def_Id));
+ end if;
+
+ -- Non-interface types
+
+ elsif Has_Invariants (Def_Id) then
Build_Invariant_Procedure_Body (Def_Id);
end if;
This patch corrects an issue outlined by AI12-0150-1 (text below) and changes class-wide type invariant procedures to avoid expensive dynamic dispatching. To accomplish this changes to most calls to Build_Invariant_Procedure_Body and Build_Invariant_Procedure_Declaration were made to handle the special case of interface types, and the replacement of parent to derived type for a type's current instance within the generated invariant procedure needed to be overhauled. Following this patch, external references within class-wide type invariants will function properly but there is no other user-facing change. AI12-0150-1: "For an invariant check on a value of type T1 based on a class-wide invariant expression inherited from an ancestor type T, any operations within the invariant expression that were resolved as primitive operations of the (notional) formal derived type NT, are in the evaluation of the invariant expression for the check on T1 bound to the corresponding operations of type T1." ------------ -- Source -- ------------ -- inv_aspects.ads with Parent_Reference; use Parent_Reference; package Inv_Aspects is ------------------------------------ -- Derivation without overriding -- ------------------------------------ type Par_1 is tagged private with Type_Invariant'Class => A (Par_1); -- own: A (Par_1) -- inheritable: A (Par_1) -- CHECKED: A (Par_1) function A (Obj : Par_1) return Boolean; type Deriv_1 is new Par_1 with private; -- inherited: A (Par_1) -- CHECKED: A (Par_1) -------------------------------- -- Derivation with overriding -- -------------------------------- type Par_2 is tagged private with Type_Invariant'Class => B (Par_2); -- own: B (Par_2) -- inheritable: B (Par_2) -- CHECKED: B (Par_2) function B (Obj : Par_2) return Boolean; type Deriv_2 is new Par_2 with private with Type_Invariant'Class => B (Deriv_2); -- inherited: B (Par_2) overridden by B (Deriv_2) -- CHECKED: B (Deriv_2) -- overriding function B (Obj : Deriv_2) return Boolean; ------------------------------------ -- Derivation with Inv overriding -- ------------------------------------ type Par_3 is tagged private with Type_Invariant'Class => C (Par_3); -- own: C (Par_3) -- inheritable: C (Par_3) -- CHECKED: C (Par_3) function C (Obj : Par_3) return Boolean; type Deriv_3 is new Par_3 with private with Type_Invariant'Class => D (Deriv_3); -- own: D (Deriv_3) -- inherited: C (Par_3) -- CHECKED: C (Par_3) -- D (Deriv_3) function D (Obj : Deriv_3) return Boolean; ------------------------------------------------ -- Derivation with overriding, Inv overriding -- ------------------------------------------------ type Par_4 is tagged private with Type_Invariant'Class => E (Par_4); -- own: E (Par_4) -- inheritable: E (Par_4) -- CHECKED: E (Par_4) function E (Obj : Par_4) return Boolean; type Deriv_4 is new Par_4 with private with Type_Invariant'Class => E (Deriv_4); -- own: E (Deriv_4) -- inherited: E (Par_4) overridden by E (Deriv_4) -- CHECKED: E (Deriv_4) x 2 (from derivation and component) overriding function E (Obj : Deriv_4) return Boolean; ---------------------------------------- -- Derivation with partial overriding -- ---------------------------------------- type Par_5 is tagged private with Type_Invariant'Class => F (Par_5) and G (Par_5); -- own: F (Par_5) -- G (Par_5) -- inheritable: F (Par_5) -- G (Par_5) function F (Obj : Par_5) return Boolean; function G (Obj : Par_5) return Boolean; type Deriv_5 is new Par_5 with private; -- inherited: F (Par_5) overridden by F (Deriv_5) -- G (Par_5) -- CHECKED: F (Deriv_5) -- G (Par_5) overriding function F (Obj : Deriv_5) return Boolean; ------------------------------------------- -- Hidden derivation without overriding -- ------------------------------------------- type Par_6 is tagged private with Type_Invariant'Class => H (Par_6); -- own: H (Par_6) -- inheritable: H (Par_6) -- CHECKED: H (Par_6) function H (Obj : Par_6) return Boolean; type Deriv_6 is tagged private; -- inherited: H (Par_6) -- CHECKED: H (Par_6) --------------------------------------- -- Hidden derivation with overriding -- --------------------------------------- type Par_7 is tagged private with Type_Invariant'Class => I (Par_7); -- own: I (Par_7) -- inheritable: I (Par_7) -- CHECKED: I (Par_7) function I (Obj : Par_7) return Boolean; type Deriv_7 is tagged private; -- inherited: I (Par_7) overridden by I (Deriv_7) -- CHECKED: I (Deriv_7) ----------------------------------------------- -- Hidden derivation with partial overriding -- ----------------------------------------------- type Par_8 is tagged private with Type_Invariant'Class => J (Par_8) and K (Par_8) and L (Par_8); -- own: J (Par_8) -- K (Par_8) -- L (Par_8) -- inheritable: J (Par_8) -- K (Par_8) -- L (Par_8) -- CHECKED: J (Par_8) -- K (Par_8) -- L (Par_8) function J (Obj : Par_8) return Boolean; function K (Obj : Par_8) return Boolean; function L (Obj : Par_8) return Boolean; type Deriv_8 is tagged private; -- inherited: J (Par_8) overridden by J (Deriv_8) -- K (Par_8) overridden by K (Deriv_8) -- L (Par_8) -- CHECKED: J (Deriv_8) -- K (Deriv_8) -- L (Par_8) function J (Obj : Deriv_8) return Boolean; ----------------------------------- -- Long chain without overriding -- ----------------------------------- type Deriv_9 is new Deriv_1 with private; -- inherited: A (Par_1) -- CHECKED: A (Par_1) -------------------------------- -- Long chain with overriding -- -------------------------------- type Deriv_10 is new Deriv_2 with private; -- inherited: B (Deriv_2) -- CHECKED: B (Deriv_2) ------------------------- -- Multiple invariants -- ------------------------- type Deriv_11 is tagged private with Type_Invariant'Class => A2 (Deriv_11); -- own: A2 (Deriv_11) -- B2 (Deriv_11) -- inheritable: A2 (Deriv_11) -- B2 (Deriv_11) -- CHEDKED: A2 (Deriv_11) -- B2 (Deriv_11) function A2 (Obj : Deriv_11) return Boolean; function B2 (Obj : Deriv_11) return Boolean; --------------- -- Component -- --------------- type Deriv_12 is tagged private with Type_Invariant'Class => C2 (Deriv_12); -- own: C2 (Deriv_12) -- inheritable: C2 (Deriv_12) -- CHECKED: C2 (Deriv_12) function C2 (Obj : Deriv_12) return Boolean; type Rec_Deriv_12 is private; -- inherited: C2 (Deriv_12) -- CHEDKED: C2 (Deriv_12) x 2 (from derivation and component) --------------- -- Interface -- --------------- type Iface_1 is interface with Type_Invariant'Class => D2 (Iface_1); -- own: D2 (Iface_1) -- inheritable: D2 (Iface_2) -- CHECKED: none function D2 (Obj : Iface_1) return Boolean is abstract; type Deriv_13 is new Iface_1 with private with Type_Invariant'Class => E2 (Deriv_13); -- own: E2 (Deriv_13) -- inheritable: E2 (Deriv_13) -- inherited: D2 (Iface_1) overridden by D2 (Deriv_13) -- CHECKED: D2 (Deriv_13) -- E2 (Deriv_13) overriding function D2 (Obj : Deriv_13) return Boolean; function E2 (Obj : Deriv_13) return Boolean; --------------------------------------- -- Multiple invariants and component -- --------------------------------------- type Deriv_14 is tagged private with Type_Invariant'Class => F2 (Deriv_14); -- own: F2 (Deriv_14) -- G2 (Deriv_14) -- inheritable: F2 (Deriv_14) -- CHECKED: F2 (Deriv_14) -- G2 (Deriv_14) function F2 (Obj : Deriv_14) return Boolean; function G2 (Obj : Deriv_14) return Boolean; type Rec_Deriv_14 is private; -- inherited: F2 (Deriv_14) -- CHECKED: F2 (Deriv_14) x 2 (from derivation and component) -- G2 (Deriv_14) --------------------------------------- -- Mutliple invariants and interface -- --------------------------------------- type Iface_2 is interface with Type_Invariant'Class => H2 (Iface_2); -- own: H2 (Iface_2) -- inheritable: H2 (Iface_2) -- CHECKED: none function H2 (Obj : Iface_2) return Boolean is abstract; type Deriv_15 is new Iface_2 with private with Type_Invariant'Class => I2 (Deriv_15); -- own: I2 (Deriv_15) -- J2 (Deriv_15) -- inherited: H2 (Iface_2) overridden by H2 (Deriv_15) -- CHECKED: H2 (Deriv_15) -- I2 (Deriv_15) -- J2 (Deriv_15) overriding function H2 (Obj : Deriv_15) return Boolean; function I2 (Obj : Deriv_15) return Boolean; function J2 (Obj : Deriv_15) return Boolean; --------------------------------------------------- -- Multiple invariants, component, and interface -- --------------------------------------------------- type Iface_3 is interface with Type_Invariant'Class => K2 (Iface_3); -- own: K2 (Iface_3) -- inheritable: K2 (Iface_3) -- CHECKED: none function K2 (Obj : Iface_3) return Boolean is abstract; type Deriv_16 is tagged private with Type_Invariant'Class => L2 (Deriv_16); -- own: L2 (Deriv_16) -- M2 (Deriv_16) -- inheritable: L2 (Deriv_16) -- CHECKED: L2 (Deriv_16) -- M2 (Deriv_16) function L2 (Obj : Deriv_16) return Boolean; function M2 (Obj : Deriv_16) return Boolean; type Rec_Deriv_16 is private; -- inherited: K2 (Iface_3) overridden by K2 (Rec_Deriv_16) -- CHECKED: K2 (Rec_Deriv_16) -- L2 (Deriv_16) x 2 (from derivation and component) -- M2 (Deriv_16) -------------------- -- Protected type -- -------------------- type Iface_4 is limited interface with Type_Invariant'Class => O2 (Iface_4); -- own: O2 (Iface_4) -- inheritable: O2 (Iface_4) -- CHECKED: none function O2 (Obj : Iface_4) return Boolean is abstract; protected type Prot_Deriv_21 is new Iface_4 with overriding function O2 return Boolean; end; -- inherited: O2 (Iface_4) overridden by O2 (Prot_Deriv_21) -- CHECKED: O2 (Prot_Deriv_21) protected type Prot_Deriv_18 is new Iface_4 with procedure Ignore; end; -- inherited: O2 (Iface_4) overridden by O2 (Prot_Deriv_18) -- CHECKED: O2 (Prot_Deriv_18) overriding function O2 (Obj : Prot_Deriv_18) return Boolean; type Prot_Deriv_A is limited private; -- own: D3 (Prot_Deriv_A) -- inheritable: none -- CHECKED: D3 (Prot_Deriv_A) type Prot_Deriv_B is limited private with Type_Invariant => B3 (Prot_Deriv_B); -- own: B3 (Prot_Deriv_B) -- CHECKED: B3 (Prot_Deriv_B) function B3 (Obj : Prot_Deriv_B) return Boolean; type Iface_Sync_1 is synchronized interface with Type_Invariant'Class => C3 (Iface_Sync_1); -- own: C3 (Iface_Sync_1) -- inheritable: C3 (Iface_Sync_1) -- CHECKED: none function C3 (Obj : Iface_Sync_1) return Boolean is abstract; type Prot_Deriv_C is synchronized new Iface_Sync_1 with private with Type_Invariant'Class => True;-- C3 (Prot_Deriv_C); -- own: F3 (Prot_Deriv_C) -- inherited: C3 (Iface_Sync_1) overridden by C3 (Prot_Deriv_C) -- CHECKED: F3 (Prot_Deriv_C) -- C3 (Prot_Deriv_C) --------------- -- Task type -- --------------- type Iface_5 is limited interface with Type_Invariant'Class => P2 (Iface_5); -- own: P2 (Iface_5) -- inheritable: P2 (Iface_5) -- CHECKED: none function P2 (Obj : Iface_5) return Boolean is abstract; task type Task_Deriv_20 is new Iface_5 with entry Ignore; end Task_Deriv_20; -- inherited: P2 (Iface_5) overridden by P2 (Task_Deriv_20) -- CHECKED: P2 (Task_Deriv_20) overriding function P2 (Obj : Task_Deriv_20) return Boolean; type Task_Deriv_A is limited private; -- own: D4 (Task_Deriv_A) -- inheritable: none -- CHECKED: D4 (Task_Deriv_A) type Task_Deriv_B is limited private with Type_Invariant => B4 (Task_Deriv_B); -- own: B4 (Task_Deriv_B) -- CHECKED: B4 (Task_Deriv_B) function B4 (Obj : Task_Deriv_B) return Boolean; type Iface_Sync_2 is synchronized interface with Type_Invariant'Class => C4 (Iface_Sync_2); -- own: C4 (Iface_Sync_2) -- inheritable: C4 (Iface_Sync_2) -- CHECKED: none function C4 (Obj : Iface_Sync_2) return Boolean is abstract; type Task_Deriv_C is synchronized new Iface_Sync_2 with private with Type_Invariant'Class => True;-- C4 (Task_Deriv_C); -- own: F4 (Task_Deriv_C) -- inherited: C4 (Iface_Sync_2) overridden by C4 (Task_Deriv_C) -- CHECKED: F4 (Task_Deriv_C) -- C4 (Task_Deriv_C) ------------------------ -- External reference -- ------------------------ type Child_Deriv_1 is new Parent_Deriv_1 with null record; -- inherited: Get_Val_1 (Parent_Deriv_1) -- overridden by Get_Val_1 (Child_Deriv_1) -- CHECKED: Get_Val_1 (Child_Deriv_1) overriding function Get_Val_1 (Obj : Child_Deriv_1) return Integer; type Child_Deriv_2 is new Parent_Deriv_2 with null record; -- inherited: Get_Val_2 (Parent_Deriv_2) -- overridden by Get_Val_2 (Child_Deriv_2) -- CHECKED: Get_Val_2 (Child_Deriv_2) overriding function Get_Val_2 (Obj : Child_Deriv_2) return Integer; procedure Ref_2 is null; type Child_Deriv_3 is new Parent_Deriv_3 with null record; -- inherited: Get_Val_3 (Parent_Deriv_3) -- overridden by Get_Val_3 (Child_Deriv_3) -- CHECKED: Get_Val_3 (Child_Deriv_3) overriding function Get_Val_3 (Obj : Child_Deriv_3) return Integer; function Ref_3 return Integer is (12); ------------------- -- Discriminants -- ------------------- Arg : Boolean := True; type Desc_Deriv_1 (Arg : Boolean) is tagged private with Type_Invariant'Class => Arg and A5 (Desc_Deriv_1); -- own: A5 (Desc_Deriv_1) -- inherited: none -- CHECKED: A5 (Desc_Deriv_1) function A5 (Obj : Desc_Deriv_1) return Boolean; type Desc_Deriv_2 (Arg : Boolean) is limited private with Type_Invariant => Arg and B5 (Desc_Deriv_2); -- own: B5 (Desc_Deriv_2) -- inherited: none -- CHECKED: B5 (Desc_Deriv_2) function B5 (Obj : Desc_Deriv_2) return Boolean; type Desc_Deriv_3 (Arg : Boolean) is limited private with Type_Invariant => Arg and C5 (Desc_Deriv_3); -- own: C5 (Desc_Deriv_3) -- inherited: none -- CHECKED: C5 (Desc_Deriv_3) function C5 (Obj : Desc_Deriv_3) return Boolean; type Desc_Deriv_4 (Arg : Boolean) is tagged private; -- own: D5 (Desc_Deriv_4) -- inherited: none -- CHECKED: D5 (Desc_Deriv_4) ----------- -- Mix 1 -- ----------- type Typ_1 is tagged private with Type_Invariant'Class => M (Typ_1) and N (Typ_1) and O (Typ_1) and P (Typ_1) and Q (Typ_1); -- own: M (Typ_1) -- N (Typ_1) -- O (Typ_1) -- P (Typ_1) -- Q (Typ_1) -- inheritable: M (Typ_1) -- N (Typ_1) -- O (Typ_1) -- P (Typ_1) -- Q (Typ_1) -- CHECKED: M (Typ_1) -- N (Typ_1) -- O (Typ_1) -- P (Typ_1) -- Q (Typ_1) function M (Obj : Typ_1) return Boolean; function N (Obj : Typ_1) return Boolean; function O (Obj : Typ_1) return Boolean; function P (Obj : Typ_1) return Boolean; function Q (Obj : Typ_1) return Boolean; type Typ_2 is new Typ_1 with private; -- inherited: M (Typ_1) overridden by M (Typ_2) -- N (Typ_1) overridden by N (Typ_2) -- O (Typ_1) -- P (Typ_1) -- Q (Typ_1) -- CHECKED: M (Typ_2) -- N (Typ_2) -- O (Typ_1) -- P (Typ_1) -- Q (Typ_1) overriding function M (Obj : Typ_2) return Boolean; type Typ_3 is new Typ_2 with private; -- inherited: M (Typ_1) overridden by M (Typ_2) -- N (Typ_1) overridden by N (Typ_2) -- O (Typ_1) overridden by O (Typ_3) -- P (Typ_1) overridden by P (Typ_3) -- Q (Typ_1) -- CHECKED: M (Typ_2) -- N (Typ_2) -- O (Typ_3) -- P (Typ_3) -- Q (Typ_1) overriding function O (Obj : Typ_3) return Boolean; private protected type Prot_Deriv_A with Type_Invariant => Prot_Deriv_A.D3 is function D3 return Boolean; end Prot_Deriv_A; protected type Prot_Deriv_B is end Prot_Deriv_B; protected type Prot_Deriv_C with Type_Invariant => Prot_Deriv_C.F3 is new Iface_Sync_1 with function F3 return Boolean; end Prot_Deriv_C; overriding function C3 (Obj : Prot_Deriv_C) return Boolean; task type Task_Deriv_A with Type_Invariant => D4 (Task_Deriv_A) is end Task_Deriv_A; function D4 (Obj : Task_Deriv_A) return Boolean; task type Task_Deriv_B is end Task_Deriv_B; task type Task_Deriv_C with Type_Invariant => F4 (Task_Deriv_C) is new Iface_Sync_2 with end Task_Deriv_C; overriding function C4 (Obj : Task_Deriv_C) return Boolean; function F4 (Obj : Task_Deriv_C) return Boolean; type Deriv_11 is tagged null record with Type_Invariant => B2 (Deriv_11); type Deriv_12 is tagged null record; type Deriv_13 is new Iface_1 with null record; type Deriv_14 is tagged null record with Type_Invariant => G2 (Deriv_14); type Deriv_15 is new Iface_2 with null record with Type_Invariant => J2 (Deriv_15); type Deriv_16 is tagged null record with Type_Invariant => M2 (Deriv_16); type Rec_Deriv_12 is new Deriv_12 with record Deriv : Deriv_12; end record; type Rec_Deriv_14 is new Deriv_14 with record Deriv : Deriv_14; end record; type Rec_Deriv_16 is new Deriv_16 and Iface_3 with record Deriv : Deriv_16; end record; overriding function K2 (Obj : Rec_Deriv_16) return Boolean; type Par_1 is tagged null record; type Par_2 is tagged null record; type Par_3 is tagged null record; type Par_4 is tagged null record; type Par_5 is tagged null record; type Par_6 is tagged null record; type Par_7 is tagged null record; type Par_8 is tagged null record; type Deriv_1 is new Par_1 with null record; type Deriv_2 is new Par_2 with null record; type Deriv_3 is new Par_3 with null record; type Deriv_4 is new Par_4 with null record; type Deriv_5 is new Par_5 with null record; type Deriv_6 is new Par_6 with null record; type Deriv_7 is new Par_7 with null record; overriding function B (Obj : Deriv_2) return BOolean; overriding function I (Obj : Deriv_7) return Boolean; type Deriv_8 is new Par_8 with null record; overriding function K (Obj : Deriv_8) return Boolean; type Deriv_9 is new Deriv_1 with null record; type Deriv_10 is new Deriv_2 with null record; type Typ_1 is tagged null record; type Typ_2 is new Typ_1 with null record; overriding function N (Obj : Typ_2) return Boolean; type Typ_3 is new Typ_2 with null record; overriding function P (Obj : Typ_3) return Boolean; type Desc_Deriv_1 (Arg : Boolean) is tagged null record; protected type Desc_Deriv_2 (Arg : Boolean) is end Desc_Deriv_2; task type Desc_Deriv_3 (Arg : Boolean) is end Desc_Deriv_3; type Desc_Deriv_4 (Arg : Boolean) is tagged null record with Type_Invariant => Arg and D5 (Desc_Deriv_4); function D5 (Obj : Desc_Deriv_4) return Boolean; end Inv_Aspects; ---------------------------- -- Compilation and output -- ---------------------------- & gnatmake -gnata -q inv_main.adb & inv_main Deriv_1: OK Deriv_2: OK Deriv_3: OK Deriv_4: OK Deriv_5: OK Deriv_6: OK Deriv_7: OK Deriv_8: OK Deriv_9: OK Deriv_10: OK Deriv_11: OK Rec_Deriv_12: OK Deriv_13: OK Rec_Deriv_14: OK Deriv_15: OK Rec_Deriv_16: OK Child_Deriv_1: OK Child_Deriv_2: OK Child_Deriv_3: OK Prot_Deriv_18: OK Prot_Deriv_21: OK Task_Deriv_20: OK Par_1: OK Par_2: OK Par_3: OK Par_4: OK Par_5: OK Par_6: OK Par_7: OK Par_8: OK Typ_1: OK Typ_2: OK Typ_3: OK Task_Deriv_A: OK Task_Deriv_B: OK Task_Deriv_C: OK Prot_Deriv_A: OK Prot_Deriv_B: OK Prot_Deriv_C: OK Desc_Deriv_1: OK Desc_Deriv_2: OK Desc_Deriv_3: OK Desc_Deriv_4: OK Deriv_1: OK Deriv_2: OK Deriv_3: OK Deriv_4: OK Deriv_5: OK Deriv_6: OK Deriv_7: OK Deriv_8: OK Deriv_9: OK Deriv_10: OK Deriv_11: OK Rec_Deriv_12: OK Deriv_13: OK Rec_Deriv_14: OK Deriv_15: OK Rec_Deriv_16: OK Par_1: OK Par_2: OK Par_3: OK Par_4: OK Par_5: OK Par_6: OK Par_7: OK Par_8: OK Typ_1: OK Typ_2: OK Typ_3: OK Tested on x86_64-pc-linux-gnu, committed on trunk 2017-04-25 Justin Squirek <squirek@adacore.com> * exp_ch3.adb (Freeze_Type): Add condition to always treat interface types as a partial view of a private type for the generation of invariant procedure bodies. * exp_util.adb, exp_util.ads (Add_Inherited_Invariants): Add a condition to get the Corresponding_Record_Type for concurrent types, add condition to return in the absence of a class in the pragma, remove call to Replace_Type_References, and add call to Replace_References. (Add_Interface_Invariatns), (Add_Parent_Invariants): Modify call to Add_Inherited_Invariants to including the working type T. (Add_Own_Invariants): Remove legacy condition for separate units, remove dispatching for ASIS and save a copy of the expression in the pragma expression. (Build_Invariant_Procedure_Body): Default initalize vars, remove return condition on interfaces, always use the private type for interfaces, and move the processing of types until after the processing of invariants for the full view. (Build_Invariant_Procedure_Declaration): Remove condition to return if an interface type is encountered and add condition to convert the formal parameter to its class-wide counterpart if Work_Typ is abstract. (Replace_Type): Add call to Remove_Controlling_Arguments. (Replace_Type_Ref): Remove class-wide dispatching for the current instance of the type. (Replace_Type_References): Remove parameter "Derived" (Remove_Controlling_Arguments): Created in order to removing the controlliong argument from calls to primitives in the case of the formal parameter being an class-wide abstract type. * sem_ch3.adb (Build_Assertion_Bodies_For_Type): Almost identical to the change made to Freeze_Type in exp_ch3. Add a condition to treat interface types as a partial view. * sem_prag.adb (Analyze_Pragma): Modify parameters in the call to Build_Invariant_Procedure_Declaration to properly generate a "partial" invariant procedure when Typ is an interface.