[Ada] Ada2020: AI12-0195 overriding class-wide pre/post conditions
gcc/ada/ * contracts.adb (Process_Spec_Postconditions): Add missing support for aliased subprograms and handle wrappers of class-wide pre/post conditions. (Process_Inherited_Preconditions): Add missing support for aliased subprograms and handle wrappers of class-wide pre/post conditions. * einfo.ads (Class_Wide_Clone): Fix typo. (Is_Class_Wide_Clone): Removed since it is not referenced. (Is_Wrapper): Documenting new flag. (LSP_Subprogram): Documenting new attribute. * exp_ch3.adb (Make_Controlling_Function_Wrappers): Decorate wrapper as Is_Wrapper and adjust call to Override_Dispatching_Operation. * freeze.adb (Build_Inherited_Condition_Pragmas): Fix typo in documentation. (Check_Inherited_Conditions): Handle LSP wrappers; ensure correct decoration of LSP wrappers. * gen_il-fields.ads (Is_Class_Wide_Clone): Removed. (Is_Wrapper): Added. (LSP_Subprogram): Added. * gen_il-gen-gen_entities.adb (Is_Class_Wide_Clone): Removed. (Is_Wrapper): Added. (LSP_Subprogram): Added. * gen_il-internals.adb (Image): Adding uppercase image of LSP_Subprogram. * sem_ch6.adb (New_Overloaded_Entity): Fix decoration of LSP wrappers. * sem_disp.ads (Override_Dispatching_Operation): Remove parameter Is_Wrapper; no longer needed. * sem_disp.adb (Check_Dispatching_Operation): Adjust assertion. (Override_Dispatching_Operation): Remove parameter Is_Wrapper; no longer needed. * treepr.adb (Image): Adding uppercase image of LSP_Subprogram.
This commit is contained in:
Javier Miranda
Pierre-Marie de Rodat
parent
4edcee5b2b
commit
c37c13e15e
|
|
@ -2610,7 +2610,21 @@ package body Contracts is
|
|||
|
||||
for Index in Subps'Range loop
|
||||
Subp_Id := Subps (Index);
|
||||
Items := Contract (Subp_Id);
|
||||
|
||||
if Present (Alias (Subp_Id)) then
|
||||
Subp_Id := Ultimate_Alias (Subp_Id);
|
||||
end if;
|
||||
|
||||
-- Wrappers of class-wide pre/post conditions reference the
|
||||
-- parent primitive that has the inherited contract.
|
||||
|
||||
if Is_Wrapper (Subp_Id)
|
||||
and then Present (LSP_Subprogram (Subp_Id))
|
||||
then
|
||||
Subp_Id := LSP_Subprogram (Subp_Id);
|
||||
end if;
|
||||
|
||||
Items := Contract (Subp_Id);
|
||||
|
||||
if Present (Items) then
|
||||
Prag := Pre_Post_Conditions (Items);
|
||||
|
|
@ -2892,7 +2906,21 @@ package body Contracts is
|
|||
|
||||
for Index in Subps'Range loop
|
||||
Subp_Id := Subps (Index);
|
||||
Items := Contract (Subp_Id);
|
||||
|
||||
if Present (Alias (Subp_Id)) then
|
||||
Subp_Id := Ultimate_Alias (Subp_Id);
|
||||
end if;
|
||||
|
||||
-- Wrappers of class-wide pre/post conditions reference the
|
||||
-- parent primitive that has the inherited contract.
|
||||
|
||||
if Is_Wrapper (Subp_Id)
|
||||
and then Present (LSP_Subprogram (Subp_Id))
|
||||
then
|
||||
Subp_Id := LSP_Subprogram (Subp_Id);
|
||||
end if;
|
||||
|
||||
Items := Contract (Subp_Id);
|
||||
|
||||
if Present (Items) then
|
||||
Prag := Pre_Post_Conditions (Items);
|
||||
|
|
|
|||
|
|
@ -612,7 +612,7 @@ package Einfo is
|
|||
|
||||
-- Class_Wide_Clone
|
||||
-- Defined on subprogram entities. Set if the subprogram has a class-wide
|
||||
-- ore- or postcondition, and the expression contains calls to other
|
||||
-- pre- or postcondition, and the expression contains calls to other
|
||||
-- primitive funtions of the type. Used to implement properly the
|
||||
-- semantics of inherited operations whose class-wide condition may
|
||||
-- be different from that of the ancestor (See AI012-0195).
|
||||
|
|
@ -2385,12 +2385,6 @@ package Einfo is
|
|||
-- Defined in all entities. Set only for defining entities of program
|
||||
-- units that are child units (but False for subunits).
|
||||
|
||||
-- Is_Class_Wide_Clone
|
||||
-- Defined on subprogram entities. Set for subprograms built in order
|
||||
-- to implement properly the inheritance of class-wide pre- or post-
|
||||
-- conditions when the condition contains calls to other primitives
|
||||
-- of the ancestor type. Used to implement AI12-0195.
|
||||
|
||||
-- Is_Class_Wide_Equivalent_Type
|
||||
-- Defined in record types and subtypes. Set to True, if the type acts
|
||||
-- as a class-wide equivalent type, i.e. the Equivalent_Type field of
|
||||
|
|
@ -3408,6 +3402,11 @@ package Einfo is
|
|||
-- Defined in package entities. Indicates that the package has been
|
||||
-- created as a wrapper for a subprogram instantiation.
|
||||
|
||||
-- Is_Wrapper
|
||||
-- Defined in subprogram entities. Indicates that it has been created as
|
||||
-- a wrapper to handle inherited class-wide pre/post conditions that call
|
||||
-- overridden primitives or as a wrapper of a controlling function.
|
||||
|
||||
-- Itype_Printed
|
||||
-- Defined in all type and subtype entities. Set in Itypes if the Itype
|
||||
-- has been printed by Sprint. This is used to avoid printing an Itype
|
||||
|
|
@ -4715,6 +4714,12 @@ package Einfo is
|
|||
-- Defined in functions and procedures which have been classified as
|
||||
-- Is_Primitive_Wrapper. Set to the entity being wrapper.
|
||||
|
||||
-- LSP_Subprogram
|
||||
-- Defined in subprogram entities. Set on wrappers created to handle
|
||||
-- inherited class-wide pre/post conditions that call overridden
|
||||
-- primitives. It references the parent primitive that has the
|
||||
-- class-wide pre/post conditions.
|
||||
|
||||
---------------------------
|
||||
-- Renaming and Aliasing --
|
||||
---------------------------
|
||||
|
|
@ -5487,6 +5492,7 @@ package Einfo is
|
|||
-- Protection_Object (for concurrent kind)
|
||||
-- Subps_Index (non-generic case only)
|
||||
-- Interface_Alias
|
||||
-- LSP_Subprogram (non-generic case only)
|
||||
-- Overridden_Operation
|
||||
-- Wrapped_Entity (non-generic case only)
|
||||
-- Extra_Formals
|
||||
|
|
@ -5546,6 +5552,7 @@ package Einfo is
|
|||
-- Is_Private_Primitive (non-generic case only)
|
||||
-- Is_Pure
|
||||
-- Is_Visible_Lib_Unit
|
||||
-- Is_Wrapper
|
||||
-- Needs_No_Actuals
|
||||
-- Requires_Overriding (non-generic case only)
|
||||
-- Return_Present
|
||||
|
|
@ -5687,6 +5694,7 @@ package Einfo is
|
|||
-- Linker_Section_Pragma
|
||||
-- Contract
|
||||
-- Import_Pragma
|
||||
-- LSP_Subprogram
|
||||
-- SPARK_Pragma
|
||||
-- Default_Expressions_Processed
|
||||
-- Has_Nested_Subprogram
|
||||
|
|
@ -5697,6 +5705,7 @@ package Einfo is
|
|||
-- Is_Machine_Code_Subprogram
|
||||
-- Is_Primitive
|
||||
-- Is_Pure
|
||||
-- Is_Wrapper
|
||||
-- SPARK_Pragma_Inherited
|
||||
-- Interface_Name $$$
|
||||
-- Renamed_Entity $$$
|
||||
|
|
@ -5841,6 +5850,7 @@ package Einfo is
|
|||
-- Protection_Object (for concurrent kind)
|
||||
-- Subps_Index (non-generic case only)
|
||||
-- Interface_Alias
|
||||
-- LSP_Subprogram (non-generic case only)
|
||||
-- Overridden_Operation (never for init proc)
|
||||
-- Wrapped_Entity (non-generic case only)
|
||||
-- Extra_Formals
|
||||
|
|
@ -5899,6 +5909,7 @@ package Einfo is
|
|||
-- Is_Private_Descendant
|
||||
-- Is_Private_Primitive (non-generic case only)
|
||||
-- Is_Pure
|
||||
-- Is_Wrapper
|
||||
-- Is_Valued_Procedure
|
||||
-- Is_Visible_Lib_Unit
|
||||
-- Needs_No_Actuals
|
||||
|
|
|
|||
|
|
@ -9703,10 +9703,10 @@ package body Exp_Ch3 is
|
|||
-- to override interface primitives.
|
||||
|
||||
Mutate_Ekind (Defining_Unit_Name (Func_Spec), E_Function);
|
||||
Set_Is_Wrapper (Defining_Unit_Name (Func_Spec));
|
||||
|
||||
Override_Dispatching_Operation
|
||||
(Tag_Typ, Subp, New_Op => Defining_Unit_Name (Func_Spec),
|
||||
Is_Wrapper => True);
|
||||
(Tag_Typ, Subp, New_Op => Defining_Unit_Name (Func_Spec));
|
||||
end if;
|
||||
|
||||
<<Next_Prim>>
|
||||
|
|
|
|||
|
|
@ -1474,7 +1474,7 @@ package body Freeze is
|
|||
-- pragmas force the creation of a wrapper for the inherited operation.
|
||||
-- If the ancestor is being overridden, the pragmas are constructed only
|
||||
-- to verify their legality, in case they contain calls to other
|
||||
-- primitives that may haven been overridden.
|
||||
-- primitives that may have been overridden.
|
||||
|
||||
---------------------------------------
|
||||
-- Build_Inherited_Condition_Pragmas --
|
||||
|
|
@ -1558,6 +1558,15 @@ package body Freeze is
|
|||
then
|
||||
Par_Prim := Overridden_Operation (Prim);
|
||||
|
||||
-- When the primitive is an LSP wrapper we climb to the parent
|
||||
-- primitive that has the inherited contract.
|
||||
|
||||
if Is_Wrapper (Par_Prim)
|
||||
and then Present (LSP_Subprogram (Par_Prim))
|
||||
then
|
||||
Par_Prim := LSP_Subprogram (Par_Prim);
|
||||
end if;
|
||||
|
||||
-- Analyze the contract items of the overridden operation, before
|
||||
-- they are rewritten as pragmas.
|
||||
|
||||
|
|
@ -1596,6 +1605,15 @@ package body Freeze is
|
|||
if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then
|
||||
Par_Prim := Alias (Prim);
|
||||
|
||||
-- When the primitive is an LSP wrapper we climb to the parent
|
||||
-- primitive that has the inherited contract.
|
||||
|
||||
if Is_Wrapper (Par_Prim)
|
||||
and then Present (LSP_Subprogram (Par_Prim))
|
||||
then
|
||||
Par_Prim := LSP_Subprogram (Par_Prim);
|
||||
end if;
|
||||
|
||||
-- Analyze the contract items of the parent operation, and
|
||||
-- determine whether a wrapper is needed. This is determined
|
||||
-- when the condition is rewritten in sem_prag, using the
|
||||
|
|
@ -1629,14 +1647,22 @@ package body Freeze is
|
|||
-- statement with a call.
|
||||
|
||||
declare
|
||||
Alias_Id : constant Entity_Id := Ultimate_Alias (Prim);
|
||||
Loc : constant Source_Ptr := Sloc (R);
|
||||
Par_R : constant Node_Id := Parent (R);
|
||||
New_Body : Node_Id;
|
||||
New_Decl : Node_Id;
|
||||
New_Id : Entity_Id;
|
||||
New_Spec : Node_Id;
|
||||
|
||||
begin
|
||||
-- The wrapper must be analyzed in the scope of its wrapped
|
||||
-- primitive (to ensure its correct decoration).
|
||||
|
||||
Push_Scope (Scope (Prim));
|
||||
|
||||
New_Spec := Build_Overriding_Spec (Par_Prim, R);
|
||||
New_Id := Defining_Entity (New_Spec);
|
||||
New_Decl :=
|
||||
Make_Subprogram_Declaration (Loc,
|
||||
Specification => New_Spec);
|
||||
|
|
@ -1658,9 +1684,26 @@ package body Freeze is
|
|||
Build_Class_Wide_Clone_Call
|
||||
(Loc, Decls, Par_Prim, New_Spec);
|
||||
|
||||
-- Adding minimum decoration
|
||||
|
||||
Mutate_Ekind (New_Id, Ekind (Par_Prim));
|
||||
Set_LSP_Subprogram (New_Id, Par_Prim);
|
||||
Set_Is_Wrapper (New_Id);
|
||||
|
||||
Insert_List_After_And_Analyze
|
||||
(Par_R, New_List (New_Decl, New_Body));
|
||||
|
||||
-- Ensure correct decoration
|
||||
|
||||
pragma Assert (Present (Alias (Prim)));
|
||||
pragma Assert (Present (Overridden_Operation (New_Id)));
|
||||
pragma Assert (Overridden_Operation (New_Id) = Alias_Id);
|
||||
end if;
|
||||
|
||||
pragma Assert (Is_Dispatching_Operation (Prim));
|
||||
pragma Assert (Is_Dispatching_Operation (New_Id));
|
||||
|
||||
Pop_Scope;
|
||||
end;
|
||||
end if;
|
||||
|
||||
|
|
|
|||
|
|
@ -677,7 +677,6 @@ package Gen_IL.Fields is
|
|||
Is_Character_Type,
|
||||
Is_Checked_Ghost_Entity,
|
||||
Is_Child_Unit,
|
||||
Is_Class_Wide_Clone,
|
||||
Is_Class_Wide_Equivalent_Type,
|
||||
Is_Compilation_Unit,
|
||||
Is_Completely_Hidden,
|
||||
|
|
@ -789,6 +788,7 @@ package Gen_IL.Fields is
|
|||
Is_Volatile_Type,
|
||||
Is_Volatile_Object,
|
||||
Is_Volatile_Full_Access,
|
||||
Is_Wrapper,
|
||||
Itype_Printed,
|
||||
Kill_Elaboration_Checks,
|
||||
Kill_Range_Checks,
|
||||
|
|
@ -802,6 +802,7 @@ package Gen_IL.Fields is
|
|||
Lit_Indexes,
|
||||
Lit_Strings,
|
||||
Low_Bound_Tested,
|
||||
LSP_Subprogram,
|
||||
Machine_Radix_10,
|
||||
Master_Id,
|
||||
Materialize_Entity,
|
||||
|
|
|
|||
|
|
@ -126,7 +126,6 @@ begin -- Gen_IL.Gen.Gen_Entities
|
|||
Sm (Is_Character_Type, Flag),
|
||||
Sm (Is_Checked_Ghost_Entity, Flag),
|
||||
Sm (Is_Child_Unit, Flag),
|
||||
Sm (Is_Class_Wide_Clone, Flag),
|
||||
Sm (Is_Class_Wide_Equivalent_Type, Flag),
|
||||
Sm (Is_Compilation_Unit, Flag),
|
||||
Sm (Is_Concurrent_Record_Type, Flag),
|
||||
|
|
@ -204,6 +203,7 @@ begin -- Gen_IL.Gen.Gen_Entities
|
|||
Sm (Is_Volatile_Type, Flag),
|
||||
Sm (Is_Volatile_Object, Flag),
|
||||
Sm (Is_Volatile_Full_Access, Flag),
|
||||
Sm (Is_Wrapper, Flag),
|
||||
Sm (Kill_Elaboration_Checks, Flag),
|
||||
Sm (Kill_Range_Checks, Flag),
|
||||
Sm (Low_Bound_Tested, Flag),
|
||||
|
|
@ -1088,6 +1088,7 @@ begin -- Gen_IL.Gen.Gen_Entities
|
|||
Sm (Is_Predicate_Function_M, Flag),
|
||||
Sm (Is_Primitive_Wrapper, Flag),
|
||||
Sm (Is_Private_Primitive, Flag),
|
||||
Sm (LSP_Subprogram, Node_Id),
|
||||
Sm (Mechanism, Mechanism_Type),
|
||||
Sm (Next_Inlined_Subprogram, Node_Id),
|
||||
Sm (Original_Protected_Subprogram, Node_Id),
|
||||
|
|
@ -1107,7 +1108,8 @@ begin -- Gen_IL.Gen.Gen_Entities
|
|||
-- defined concatenation operator created whenever an array is declared.
|
||||
-- We do not make normal derived operators explicit in the tree, but the
|
||||
-- concatenation operators are made explicit.
|
||||
(Sm (Extra_Accessibility_Of_Result, Node_Id)));
|
||||
(Sm (Extra_Accessibility_Of_Result, Node_Id),
|
||||
Sm (LSP_Subprogram, Node_Id)));
|
||||
|
||||
Cc (E_Procedure, Subprogram_Kind,
|
||||
-- A procedure, created by a procedure declaration or a procedure
|
||||
|
|
@ -1137,6 +1139,7 @@ begin -- Gen_IL.Gen.Gen_Entities
|
|||
Sm (Is_Primitive_Wrapper, Flag),
|
||||
Sm (Is_Private_Primitive, Flag),
|
||||
Sm (Is_Valued_Procedure, Flag),
|
||||
Sm (LSP_Subprogram, Node_Id),
|
||||
Sm (Next_Inlined_Subprogram, Node_Id),
|
||||
Sm (Original_Protected_Subprogram, Node_Id),
|
||||
Sm (Postconditions_Proc, Node_Id),
|
||||
|
|
|
|||
|
|
@ -317,6 +317,8 @@ package body Gen_IL.Internals is
|
|||
return "Is_SPARK_Mode_On_Node";
|
||||
when Local_Raise_Not_OK =>
|
||||
return "Local_Raise_Not_OK";
|
||||
when LSP_Subprogram =>
|
||||
return "LSP_Subprogram";
|
||||
when OK_To_Rename =>
|
||||
return "OK_To_Rename";
|
||||
when Referenced_As_LHS =>
|
||||
|
|
|
|||
|
|
@ -12080,9 +12080,22 @@ package body Sem_Ch6 is
|
|||
-- must check whether the target is an init_proc.
|
||||
|
||||
elsif not Is_Init_Proc (S) then
|
||||
Set_Overridden_Operation (S, E);
|
||||
Inherit_Subprogram_Contract (S, E);
|
||||
Set_Is_Ada_2022_Only (S, Is_Ada_2022_Only (E));
|
||||
|
||||
-- LSP wrappers must override the ultimate alias of their
|
||||
-- wrapped dispatching primitive E; required to traverse
|
||||
-- the chain of ancestor primitives (c.f. Map_Primitives)
|
||||
-- They don't inherit contracts.
|
||||
|
||||
if Is_Wrapper (S)
|
||||
and then Present (LSP_Subprogram (S))
|
||||
then
|
||||
Set_Overridden_Operation (S, Ultimate_Alias (E));
|
||||
else
|
||||
Set_Overridden_Operation (S, E);
|
||||
Inherit_Subprogram_Contract (S, E);
|
||||
end if;
|
||||
|
||||
Set_Is_Ada_2022_Only (S, Is_Ada_2022_Only (E));
|
||||
end if;
|
||||
|
||||
Check_Overriding_Indicator (S, E, Is_Primitive => True);
|
||||
|
|
@ -12109,10 +12122,22 @@ package body Sem_Ch6 is
|
|||
Is_Predefined_Dispatching_Operation (Alias (E)))
|
||||
then
|
||||
if Present (Alias (E)) then
|
||||
Set_Overridden_Operation (S, Alias (E));
|
||||
Inherit_Subprogram_Contract (S, Alias (E));
|
||||
Set_Is_Ada_2022_Only (S,
|
||||
Is_Ada_2022_Only (Alias (E)));
|
||||
|
||||
-- LSP wrappers must override the ultimate alias of
|
||||
-- their wrapped dispatching primitive E; required to
|
||||
-- traverse the chain of ancestor primitives (see
|
||||
-- Map_Primitives). They don't inherit contracts.
|
||||
|
||||
if Is_Wrapper (S)
|
||||
and then Present (LSP_Subprogram (S))
|
||||
then
|
||||
Set_Overridden_Operation (S, Ultimate_Alias (E));
|
||||
else
|
||||
Set_Overridden_Operation (S, Alias (E));
|
||||
Inherit_Subprogram_Contract (S, Alias (E));
|
||||
end if;
|
||||
|
||||
Set_Is_Ada_2022_Only (S, Is_Ada_2022_Only (Alias (E)));
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
|
|
|||
|
|
@ -1239,7 +1239,9 @@ package body Sem_Disp is
|
|||
or else Get_TSS_Name (Subp) = TSS_Stream_Read
|
||||
or else Get_TSS_Name (Subp) = TSS_Stream_Write
|
||||
|
||||
or else Present (Contract (Overridden_Operation (Subp)))
|
||||
or else
|
||||
(Is_Wrapper (Subp)
|
||||
and then Present (LSP_Subprogram (Subp)))
|
||||
|
||||
or else GNATprove_Mode);
|
||||
|
||||
|
|
@ -2646,8 +2648,7 @@ package body Sem_Disp is
|
|||
procedure Override_Dispatching_Operation
|
||||
(Tagged_Type : Entity_Id;
|
||||
Prev_Op : Entity_Id;
|
||||
New_Op : Entity_Id;
|
||||
Is_Wrapper : Boolean := False)
|
||||
New_Op : Entity_Id)
|
||||
is
|
||||
Elmt : Elmt_Id;
|
||||
Prim : Node_Id;
|
||||
|
|
@ -2724,7 +2725,7 @@ package body Sem_Disp is
|
|||
-- wrappers of controlling functions since (at this stage)
|
||||
-- they are not yet decorated.
|
||||
|
||||
if not Is_Wrapper then
|
||||
if not Is_Wrapper (New_Op) then
|
||||
Check_Subtype_Conformant (New_Op, Prim);
|
||||
|
||||
Set_Is_Abstract_Subprogram (Prim,
|
||||
|
|
|
|||
|
|
@ -167,13 +167,10 @@ package Sem_Disp is
|
|||
procedure Override_Dispatching_Operation
|
||||
(Tagged_Type : Entity_Id;
|
||||
Prev_Op : Entity_Id;
|
||||
New_Op : Entity_Id;
|
||||
Is_Wrapper : Boolean := False);
|
||||
New_Op : Entity_Id);
|
||||
-- Replace an implicit dispatching operation of the type Tagged_Type
|
||||
-- with an explicit one. Prev_Op is an inherited primitive operation which
|
||||
-- is overridden by the explicit declaration of New_Op. Is_Wrapper is
|
||||
-- True when New_Op is an internally generated wrapper of a controlling
|
||||
-- function. The caller checks that Tagged_Type is indeed a tagged type.
|
||||
-- is overridden by the explicit declaration of New_Op.
|
||||
|
||||
procedure Propagate_Tag (Control : Node_Id; Actual : Node_Id);
|
||||
-- If a function call given by Actual is tag-indeterminate, its controlling
|
||||
|
|
|
|||
|
|
@ -371,6 +371,8 @@ package body Treepr is
|
|||
return "Is_Elaboration_Warnings_OK_Id";
|
||||
when F_Is_RACW_Stub_Type =>
|
||||
return "Is_RACW_Stub_Type";
|
||||
when F_LSP_Subprogram =>
|
||||
return "LSP_Subprogram";
|
||||
when F_OK_To_Rename =>
|
||||
return "OK_To_Rename";
|
||||
when F_Referenced_As_LHS =>
|
||||
|
|
|
|||
Loading…
Reference in New Issue