diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 125 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 176 | ||||
| -rw-r--r-- | gcc/ada/einfo.ads | 114 | ||||
| -rw-r--r-- | gcc/ada/exp_ch3.adb | 18 | ||||
| -rw-r--r-- | gcc/ada/exp_ch7.adb | 57 | ||||
| -rw-r--r-- | gcc/ada/exp_util.adb | 1340 | ||||
| -rw-r--r-- | gcc/ada/exp_util.ads | 48 | ||||
| -rw-r--r-- | gcc/ada/nlists.adb | 23 | ||||
| -rw-r--r-- | gcc/ada/nlists.ads | 12 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 302 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.adb | 60 | ||||
| -rw-r--r-- | gcc/ada/sem_ch9.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/sem_elab.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 358 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.ads | 27 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 513 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 47 | ||||
| -rw-r--r-- | gcc/ada/sem_warn.adb | 19 | ||||
| -rw-r--r-- | gcc/ada/sinfo.adb | 16 | ||||
| -rw-r--r-- | gcc/ada/sinfo.ads | 21 |
20 files changed, 2036 insertions, 1252 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index a7921c5..8acf07e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,128 @@ +2017-01-09 Hristian Kirtchev <kirtchev@adacore.com> + + * einfo.ads, einfo.adb: Remove uses of flags Has_Default_Init_Cond, + Is_Default_Init_Cond_Procedure, and + Has_Inherited_Default_Init_Cond. Add uses of flags + Has_Own_DIC, Is_DIC_Procedure, and Has_Inherited_DIC. + (Default_Init_Cond_Procedure): Removed. + (DIC_Procedure): New routine. + (Has_Default_Init_Cond): Removed. + (Has_DIC): New routine. + (Has_Inheritable_Invariants): The attribute applies to the base type. + (Has_Inherited_Default_Init_Cond): Removed. + (Has_Inherited_DIC): New routine. + (Has_Inherited_Invariants): The attribute applies to the base type. + (Has_Own_DIC): New routine. + (Has_Own_Invariants): The attribute applies to the base type. + (Is_Default_Init_Cond_Procedure): Removed. + (Is_DIC_Procedure): New routine. + (Set_Default_Init_Cond_Procedure): Removed. + (Set_DIC_Procedure): New routine. + (Set_Has_Default_Init_Cond): Removed. + (Set_Has_Inheritable_Invariants): The attribute applies + to the base type. + (Set_Has_Inherited_Default_Init_Cond): Removed. + (Set_Has_Inherited_DIC): New routine. + (Set_Has_Inherited_Invariants): The attribute applies to the base type. + (Set_Has_Own_DIC): New routine. + (Set_Has_Own_Invariants): The attribute applies to the base type. + (Set_Is_Default_Init_Cond_Procedure): Removed. + (Set_Is_DIC_Procedure): New routine. + (Write_Entity_Flags): Update the output of all flags related to + default initial condition. + * exp_ch3.adb (Expand_N_Object_Declaration): Update the generation + of the call to the DIC procedure. + (Freeze_Type): Generate the body of the DIC procedure. + * exp_ch7.adb (Build_Invariant_Procedure_Body): Replace + all occurrences of Create_Append with Append_New_To. Do + not generate an invariant procedure for a class-wide type. + The generated body acts as a freeze action of the working type. + (Build_Invariant_Procedure_Declaration): Do not generate an + invariant procedure for a class-wide type. + (Create_Append): Removed. + * exp_util.adb: Add with and use clauses for Sem_Ch3, sem_ch6, + sem_Ch12, Sem_Disp, and GNAT.HTable. Move the handling of + class-wide pre/postcondition description and data structures from + Sem_Prag. + (Build_Class_Wide_Expression): Moved from Sem_Prag. + (Build_DIC_Call): New routine. + (Build_DIC_Procedure_Body): New routine. + (Build_DIC_Procedure_Declaration): New routine. + (Entity_Hash): Moved from Sem_Prag. + (Find_DIC_Type): New routine. + (Update_Primitives_Mapping): Reimplemented. + (Update_Primitives_Mapping_Of_Types): New routine. + * exp_util.ads (Build_Class_Wide_Expression): Moved from Sem_Prag. + (Build_DIC_Call): New routine. + (Build_DIC_Procedure_Body): New routine. + (Build_DIC_Procedure_Declaration): New routine. + (Update_Primitives_Mapping): Moved from Sem_Prag. + (Update_Primitives_Mapping_Of_Types): New routine. + * nlists.adb (Append_New): New routine. + (Append_New_To): New routine. + * nlists.ads (Append_New): New routine. + (Append_New_To): New routine. + * sem_ch3.adb (Analyze_Declarations): Do not generate the bodies + of DIC procedures here. This is now done at the end of the + visible declarations, private declarations, and at the freeze + point of a type. + (Analyze_Private_Extension_Declaration): + A private extension inherits the DIC pragma of a parent type. + (Analyze_Subtype_Declaration): No need to propagate invariant + attributes to a subtype as those apply to the base type. + (Build_Derived_Record_Type): No need to inherit invariants here + as this is now done in Build_Derived_Type. + (Build_Derived_Type): Inherit both the DIC pragma and invariants from + a parent type. + (Process_Full_View): Update the propagation of DIC attributes. + (Propagate_Default_Init_Cond_Attributes): Removed. + * sem_ch7.adb Add with and use clauses for Exp_Util. + (Analyze_Package_Specification): Create the body of the DIC + procedure at the end of the visible and private declarations. + (Preserve_Full_Attributes): Propagate DIC attributes. + * sem_ch9.adb (Analyze_Protected_Type_Declaration): Propagate + DIC attributes. + (Analyze_Task_Type_Declaration): Propagate DIC attributes. + * sem_elab.adb (Check_A_Call): Update the call to + Is_Nontrivial_Default_Init_Cond_Procedure. + * sem_prag.adb Remove the with and use clauses for + GNAT.HTable. Move the handling of class- wide pre/postcondition + description and data structures to Exp_Util. + (Analyze_Pragma): Create the declaration of the DIC procedure. There + is no need to propagate invariant-related attributes at this point + as this is done in Build_Invariant_Procedure_Declaration. + (Build_Class_Wide_Expression): Moved to Exp_Util. + (Entity_Hash): Moved to Exp_Util. + (Update_Primitives_Mapping): Moved to Exp_Util. + * sem_prag.ads (Build_Class_Wide_Expression): Moved to Exp_Util. + (Update_Primitives_Mapping): Moved to Exp_Util. + * sem_util.adb: Remove with and use clauses for Ghost + and Sem_Ch13. + (Build_Default_Init_Cond_Call): Removed. + (Build_Default_Init_Cond_Procedure_Bodies): Removed. + (Build_Default_Init_Cond_Procedure_Declaration): Removed. + (Get_Views): Reimplemented. + (Has_Full_Default_Initialization): Reimplement the section on DIC. + (Inherit_Default_Init_Cond_Procedure): Removed. + (Is_Nontrivial_Default_Init_Cond_Procedure): Removed. + (Is_Nontrivial_DIC_Procedure): New routine. + (Is_Verifiable_DIC_Pragma): New routine. + (Propagate_DIC_Attributes): New routine. + * sem_util.ads (Build_Default_Init_Cond_Call): Removed. + (Build_Default_Init_Cond_Procedure_Bodies): Removed. + (Build_Default_Init_Cond_Procedure_Declaration): Removed. + (Inherit_Default_Init_Cond_Procedure): Removed. + (Is_Nontrivial_Default_Init_Cond_Procedure): Removed. + (Is_Nontrivial_DIC_Procedure): New routine. + (Is_Verifiable_DIC_Pragma): New routine. + (Propagate_DIC_Attributes): New routine. + * sem_warn.adb (Is_OK_Fully_Initialized): Reimplement the section + on DIC. + * sinfo.ads, sinfo.adb: Add new attribute Expression_Copy along with + usage in nodes. + (Expression_Copy): New routine along with pragma Inline. + (Set_Expression_Copy): New routine along with pragma Inline. + 2017-01-06 Bob Duff <duff@adacore.com> * bindgen.adb (Gen_Adainit, Gen_Adafinal): Change diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 0e66f42..f62c139 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -290,7 +290,7 @@ package body Einfo is -- Is_Inlined_Always Flag1 -- Is_Hidden_Non_Overridden_Subpgm Flag2 - -- Has_Default_Init_Cond Flag3 + -- Has_Own_DIC Flag3 -- Is_Frozen Flag4 -- Has_Discriminants Flag5 -- Is_Dispatching_Operation Flag6 @@ -432,8 +432,8 @@ package body Einfo is -- Is_Generic_Instance Flag130 -- No_Pool_Assigned Flag131 - -- Is_Default_Init_Cond_Procedure Flag132 - -- Has_Inherited_Default_Init_Cond Flag133 + -- Is_DIC_Procedure Flag132 + -- Has_Inherited_DIC Flag133 -- Has_Aliased_Components Flag135 -- No_Strict_Aliasing Flag136 -- Is_Machine_Code_Subprogram Flag137 @@ -1527,12 +1527,6 @@ package body Einfo is return Flag39 (Base_Type (Id)); end Has_Default_Aspect; - function Has_Default_Init_Cond (Id : E) return B is - begin - pragma Assert (Is_Type (Id)); - return Flag3 (Base_Type (Id)); - end Has_Default_Init_Cond; - function Has_Delayed_Aspects (Id : E) return B is begin pragma Assert (Nkind (Id) in N_Entity); @@ -1619,19 +1613,19 @@ package body Einfo is function Has_Inheritable_Invariants (Id : E) return B is begin pragma Assert (Is_Type (Id)); - return Flag248 (Id); + return Flag248 (Base_Type (Id)); end Has_Inheritable_Invariants; - function Has_Inherited_Default_Init_Cond (Id : E) return B is + function Has_Inherited_DIC (Id : E) return B is begin pragma Assert (Is_Type (Id)); return Flag133 (Base_Type (Id)); - end Has_Inherited_Default_Init_Cond; + end Has_Inherited_DIC; function Has_Inherited_Invariants (Id : E) return B is begin pragma Assert (Is_Type (Id)); - return Flag291 (Id); + return Flag291 (Base_Type (Id)); end Has_Inherited_Invariants; function Has_Initial_Value (Id : E) return B is @@ -1693,10 +1687,16 @@ package body Einfo is return Flag110 (Id); end Has_Out_Or_In_Out_Parameter; + function Has_Own_DIC (Id : E) return B is + begin + pragma Assert (Is_Type (Id)); + return Flag3 (Base_Type (Id)); + end Has_Own_DIC; + function Has_Own_Invariants (Id : E) return B is begin pragma Assert (Is_Type (Id)); - return Flag232 (Id); + return Flag232 (Base_Type (Id)); end Has_Own_Invariants; function Has_Partial_Visible_Refinement (Id : E) return B is @@ -2155,11 +2155,11 @@ package body Einfo is return Flag74 (Id); end Is_CPP_Class; - function Is_Default_Init_Cond_Procedure (Id : E) return B is + function Is_DIC_Procedure (Id : E) return B is begin pragma Assert (Ekind_In (Id, E_Function, E_Procedure)); return Flag132 (Id); - end Is_Default_Init_Cond_Procedure; + end Is_DIC_Procedure; function Is_Descendant_Of_Address (Id : E) return B is begin @@ -4563,12 +4563,6 @@ package body Einfo is Set_Flag39 (Id, V); end Set_Has_Default_Aspect; - procedure Set_Has_Default_Init_Cond (Id : E; V : B := True) is - begin - pragma Assert (Is_Type (Id)); - Set_Flag3 (Base_Type (Id), V); - end Set_Has_Default_Init_Cond; - procedure Set_Has_Delayed_Aspects (Id : E; V : B := True) is begin pragma Assert (Nkind (Id) in N_Entity); @@ -4660,19 +4654,19 @@ package body Einfo is procedure Set_Has_Inheritable_Invariants (Id : E; V : B := True) is begin pragma Assert (Is_Type (Id)); - Set_Flag248 (Id, V); + Set_Flag248 (Base_Type (Id), V); end Set_Has_Inheritable_Invariants; - procedure Set_Has_Inherited_Default_Init_Cond (Id : E; V : B := True) is + procedure Set_Has_Inherited_DIC (Id : E; V : B := True) is begin pragma Assert (Is_Type (Id)); Set_Flag133 (Base_Type (Id), V); - end Set_Has_Inherited_Default_Init_Cond; + end Set_Has_Inherited_DIC; procedure Set_Has_Inherited_Invariants (Id : E; V : B := True) is begin pragma Assert (Is_Type (Id)); - Set_Flag291 (Id, V); + Set_Flag291 (Base_Type (Id), V); end Set_Has_Inherited_Invariants; procedure Set_Has_Initial_Value (Id : E; V : B := True) is @@ -4735,10 +4729,16 @@ package body Einfo is Set_Flag110 (Id, V); end Set_Has_Out_Or_In_Out_Parameter; + procedure Set_Has_Own_DIC (Id : E; V : B := True) is + begin + pragma Assert (Is_Type (Id)); + Set_Flag3 (Base_Type (Id), V); + end Set_Has_Own_DIC; + procedure Set_Has_Own_Invariants (Id : E; V : B := True) is begin pragma Assert (Is_Type (Id)); - Set_Flag232 (Id, V); + Set_Flag232 (Base_Type (Id), V); end Set_Has_Own_Invariants; procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True) is @@ -5243,11 +5243,11 @@ package body Einfo is Set_Flag74 (Id, V); end Set_Is_CPP_Class; - procedure Set_Is_Default_Init_Cond_Procedure (Id : E; V : B := True) is + procedure Set_Is_DIC_Procedure (Id : E; V : B := True) is begin pragma Assert (Ekind (Id) = E_Procedure); Set_Flag132 (Id, V); - end Set_Is_Default_Init_Cond_Procedure; + end Set_Is_DIC_Procedure; procedure Set_Is_Descendant_Of_Address (Id : E; V : B := True) is begin @@ -7053,39 +7053,6 @@ package body Einfo is end loop; end Declaration_Node; - --------------------------------- - -- Default_Init_Cond_Procedure -- - --------------------------------- - - function Default_Init_Cond_Procedure (Id : E) return E is - 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 else Has_Inherited_Default_Init_Cond (Id))); - - Subps := Subprograms_For_Type (Base_Type (Id)); - - 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; - --------------------- -- Designated_Type -- --------------------- @@ -7113,6 +7080,36 @@ package body Einfo is end if; end Designated_Type; + ------------------- + -- DIC_Procedure -- + ------------------- + + function DIC_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 (Base_Type (Id)); + + if Present (Subps) then + Subp_Elmt := First_Elmt (Subps); + while Present (Subp_Elmt) loop + Subp_Id := Node (Subp_Elmt); + + if Is_DIC_Procedure (Subp_Id) then + return Subp_Id; + end if; + + Next_Elmt (Subp_Elmt); + end loop; + end if; + + return Empty; + end DIC_Procedure; + ---------------------- -- Entry_Index_Type -- ---------------------- @@ -7430,6 +7427,15 @@ package body Einfo is return False; end Has_Attach_Handler; + ------------- + -- Has_DIC -- + ------------- + + function Has_DIC (Id : E) return B is + begin + return Has_Own_DIC (Id) or else Has_Inherited_DIC (Id); + end Has_DIC; + ----------------- -- Has_Entries -- ----------------- @@ -7671,7 +7677,7 @@ package body Einfo is begin pragma Assert (Is_Type (Id)); - Subps := Subprograms_For_Type (Id); + Subps := Subprograms_For_Type (Base_Type (Id)); if Present (Subps) then Subp_Elmt := First_Elmt (Subps); @@ -8407,7 +8413,7 @@ package body Einfo is begin pragma Assert (Is_Type (Id)); - Subps := Subprograms_For_Type (Id); + Subps := Subprograms_For_Type (Base_Type (Id)); if Present (Subps) then Subp_Elmt := First_Elmt (Subps); @@ -8820,28 +8826,18 @@ package body Einfo is end case; end Set_Component_Alignment; - ------------------------------------- - -- Set_Default_Init_Cond_Procedure -- - ------------------------------------- + ----------------------- + -- Set_DIC_Procedure -- + ----------------------- - procedure Set_Default_Init_Cond_Procedure (Id : E; V : E) is + procedure Set_DIC_Procedure (Id : E; V : E) is Base_Typ : Entity_Id; Subp_Elmt : Elmt_Id; Subp_Id : Entity_Id; Subps : Elist_Id; begin - -- Once set, this attribute cannot be reset - - if No (V) then - pragma Assert (No (Default_Init_Cond_Procedure (Id))); - return; - end if; - - pragma Assert - (Is_Type (Id) - and then (Has_Default_Init_Cond (Id) - or else Has_Inherited_Default_Init_Cond (Id))); + pragma Assert (Is_Type (Id)); Base_Typ := Base_Type (Id); Subps := Subprograms_For_Type (Base_Typ); @@ -8859,19 +8855,20 @@ package body Einfo is while Present (Subp_Elmt) loop Subp_Id := Node (Subp_Elmt); - if Is_Default_Init_Cond_Procedure (Subp_Id) then + if Is_DIC_Procedure (Subp_Id) then raise Program_Error; end if; Next_Elmt (Subp_Elmt); end loop; - end Set_Default_Init_Cond_Procedure; + end Set_DIC_Procedure; ----------------------------- -- Set_Invariant_Procedure -- ----------------------------- procedure Set_Invariant_Procedure (Id : E; V : E) is + Base_Typ : Entity_Id; Subp_Elmt : Elmt_Id; Subp_Id : Entity_Id; Subps : Elist_Id; @@ -8879,11 +8876,12 @@ package body Einfo is begin pragma Assert (Is_Type (Id)); - Subps := Subprograms_For_Type (Id); + Base_Typ := Base_Type (Id); + Subps := Subprograms_For_Type (Base_Typ); if No (Subps) then Subps := New_Elmt_List; - Set_Subprograms_For_Type (Id, Subps); + Set_Subprograms_For_Type (Base_Typ, Subps); end if; Subp_Elmt := First_Elmt (Subps); @@ -8907,6 +8905,7 @@ package body Einfo is ------------------------------------- procedure Set_Partial_Invariant_Procedure (Id : E; V : E) is + Base_Typ : Entity_Id; Subp_Elmt : Elmt_Id; Subp_Id : Entity_Id; Subps : Elist_Id; @@ -8914,11 +8913,12 @@ package body Einfo is begin pragma Assert (Is_Type (Id)); - Subps := Subprograms_For_Type (Id); + Base_Typ := Base_Type (Id); + Subps := Subprograms_For_Type (Base_Typ); if No (Subps) then Subps := New_Elmt_List; - Set_Subprograms_For_Type (Id, Subps); + Set_Subprograms_For_Type (Base_Typ, Subps); end if; Subp_Elmt := First_Elmt (Subps); @@ -9277,7 +9277,6 @@ package body Einfo is W ("Has_Controlling_Result", Flag98 (Id)); W ("Has_Convention_Pragma", Flag119 (Id)); W ("Has_Default_Aspect", Flag39 (Id)); - W ("Has_Default_Init_Cond", Flag3 (Id)); W ("Has_Delayed_Aspects", Flag200 (Id)); W ("Has_Delayed_Freeze", Flag18 (Id)); W ("Has_Delayed_Rep_Aspects", Flag261 (Id)); @@ -9294,7 +9293,7 @@ package body Einfo is W ("Has_Implicit_Dereference", Flag251 (Id)); W ("Has_Independent_Components", Flag34 (Id)); W ("Has_Inheritable_Invariants", Flag248 (Id)); - W ("Has_Inherited_Default_Init_Cond", Flag133 (Id)); + W ("Has_Inherited_DIC", Flag133 (Id)); W ("Has_Inherited_Invariants", Flag291 (Id)); W ("Has_Initial_Value", Flag219 (Id)); W ("Has_Loop_Entry_Attributes", Flag260 (Id)); @@ -9306,6 +9305,7 @@ package body Einfo is 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_DIC", Flag3 (Id)); W ("Has_Own_Invariants", Flag232 (Id)); W ("Has_Per_Object_Constraint", Flag154 (Id)); W ("Has_Pragma_Controlled", Flag27 (Id)); @@ -9381,8 +9381,8 @@ package body Einfo is W ("Is_Constructor", Flag76 (Id)); W ("Is_Controlled", Flag42 (Id)); W ("Is_Controlling_Formal", Flag97 (Id)); - W ("Is_Default_Init_Cond_Procedure", Flag132 (Id)); W ("Is_Descendant_Of_Address", Flag223 (Id)); + W ("Is_DIC_Procedure", Flag132 (Id)); W ("Is_Discrim_SO_Function", Flag176 (Id)); W ("Is_Discriminant_Check_Function", Flag264 (Id)); W ("Is_Dispatch_Table_Entity", Flag234 (Id)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index f42c387..fd63ac5 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -848,16 +848,6 @@ package Einfo is -- default expressions (see Freeze.Process_Default_Expressions), which -- would not only waste time, but also generate false error messages. --- Default_Init_Cond_Procedure (synthesized) --- Defined in all types. Set for private [sub]types subject to pragma --- Default_Initial_Condition, their corresponding full views and derived --- types with at least one parent subject to the pragma. Contains the --- entity of the procedure which takes a single argument of the given --- type and verifies the assumption of the pragma. --- --- 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. - -- Default_Value (Node20) -- Defined in formal parameters. Points to the node representing the -- expression for the default value for the parameter. Empty if the @@ -932,6 +922,16 @@ package Einfo is -- incomplete type, and the full type is available, then this full type -- is returned instead of the incomplete type. +-- DIC_Procedure (synthesized) +-- Defined in all type entities. Set for a private type and its full view +-- when the type is subject to pragma Default_Initial_Condition (DIC), or +-- when the type inherits a DIC pragma from a parent type. Points to the +-- entity of a procedure which takes a single argument of the given type +-- and verifies the assertion expression of the DIC pragma at runtime. + +-- 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. + -- Digits_Value (Uint17) -- Defined in floating point types and subtypes and decimal types and -- subtypes. Contains the Digits value specified in the declaration. @@ -1574,11 +1574,6 @@ package Einfo is -- value is set, but it may be overridden by an aspect declaration on -- type derivation. --- Has_Default_Init_Cond (Flag3) [base type only] --- Defined in all type entities. Set if pragma Default_Initial_Condition --- applies to a private type and by extension to its full view. This flag --- is mutually exclusive with flag Has_Inherited_Default_Init_Cond. - -- Has_Delayed_Aspects (Flag200) -- Defined in all entities. Set if the Rep_Item chain for the entity has -- one or more N_Aspect_Definition nodes chained which are not to be @@ -1600,6 +1595,11 @@ package Einfo is -- set, signalling that Freeze.Inherit_Delayed_Rep_Aspects must be called -- at the freeze point of the derived type. +-- Has_DIC (syntherized) +-- Defined in all type entities. Set for a private type and its full view +-- when the type is subject to pragma Default_Initial_Condition (DIC), or +-- when the type inherits a DIC pragma from a parent type. + -- Has_Discriminants (Flag5) -- Defined in all types and subtypes. For types that are allowed to have -- discriminants (record types and subtypes, task types and subtypes, @@ -1706,18 +1706,17 @@ package Einfo is -- will be chained to the rep item chain of the first subtype in the -- usual manner. --- Has_Inheritable_Invariants (Flag248) +-- Has_Inheritable_Invariants (Flag248) [base type only] -- 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_DIC (Flag133) [base type only] +-- Defined in all type entities. Set for a derived type which inherits +-- pragma Default_Initial_Condition from a parent type. --- Has_Inherited_Invariants (Flag291) +-- Has_Inherited_Invariants (Flag291) [base type only] -- 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 @@ -1816,10 +1815,14 @@ package Einfo is -- families. Set if they have at least one OUT or IN OUT parameter -- (allowed for functions only in Ada 2012). --- Has_Own_Invariants (Flag232) +-- Has_Own_DIC (Flag3) [base type only] +-- Defined in all type entities. Set for a private type and its full view +-- when the type is subject to pragma Default_Initial_Condition. + +-- Has_Own_Invariants (Flag232) [base type only] -- 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. +-- private type for completeness. -- Has_Partial_Visible_Refinement (Flag296) -- Defined in E_Abstract_State entities. Set when a state has at least @@ -2422,14 +2425,15 @@ package Einfo is -- Applies to all type entities, true for decimal fixed point -- types and subtypes. --- Is_Default_Init_Cond_Procedure (Flag132) --- Defined in functions and procedures. Set for a generated procedure --- which verifies the assumption of pragma Default_Initial_Condition. - -- Is_Descendant_Of_Address (Flag223) -- Defined in all entities. True if the entity is type System.Address, -- or (recursively) a subtype or derived type of System.Address. +-- Is_DIC_Procedure (Flag132) +-- Defined in functions and procedures. Set for a generated procedure +-- which verifies the assumption of pragma Default_Initial_Condition at +-- runtime. + -- Is_Discrete_Or_Fixed_Point_Type (synthesized) -- Applies to all entities, true for all discrete types and subtypes -- and all fixed-point types and subtypes. @@ -5558,16 +5562,16 @@ package Einfo is -- Has_Constrained_Partial_View (Flag187) -- Has_Controlled_Component (Flag43) (base type only) -- Has_Default_Aspect (Flag39) (base type only) - -- Has_Default_Init_Cond (Flag3) (base type only) -- Has_Delayed_Rep_Aspects (Flag261) -- Has_Discriminants (Flag5) -- Has_Dynamic_Predicate_Aspect (Flag258) -- Has_Independent_Components (Flag34) (base type only) -- Has_Inheritable_Invariants (Flag248) (base type only) - -- Has_Inherited_Default_Init_Cond (Flag133) (base type only) + -- Has_Inherited_DIC (Flag133) (base type only) -- Has_Inherited_Invariants (Flag291) (base type only) -- Has_Non_Standard_Rep (Flag75) (base type only) -- Has_Object_Size_Clause (Flag172) + -- Has_Own_DIC (Flag3) (base type only) -- Has_Own_Invariants (Flag232) (base type only) -- Has_Pragma_Preelab_Init (Flag221) -- Has_Pragma_Unreferenced_Objects (Flag212) @@ -5621,7 +5625,8 @@ package Einfo is -- Alignment_Clause (synth) -- Base_Type (synth) - -- Default_Init_Cond_Procedure (synth) + -- DIC_Procedure (synth) + -- Has_DIC (synth) -- Has_Invariants (synth) -- Implementation_Base_Type (synth) -- Invariant_Procedure (synth) @@ -6026,7 +6031,7 @@ package Einfo is -- 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_DIC_Procedure (Flag132) (non-generic case only) -- Is_Discrim_SO_Function (Flag176) -- Is_Discriminant_Check_Function (Flag264) -- Is_Eliminated (Flag124) @@ -6337,7 +6342,7 @@ package Einfo is -- Is_Asynchronous (Flag81) -- Is_Called (Flag102) (non-generic case only) -- Is_Constructor (Flag76) - -- Is_Default_Init_Cond_Procedure (Flag132) (non-generic case only) + -- Is_DIC_Procedure (Flag132) (non-generic case only) -- Is_Eliminated (Flag124) -- Is_Generic_Actual_Subprogram (Flag274) (non-generic case only) -- Is_Hidden_Non_Overridden_Subpgm (Flag2) (non-generic case only) @@ -6982,10 +6987,10 @@ package Einfo is function Has_Controlling_Result (Id : E) return B; function Has_Convention_Pragma (Id : E) return B; function Has_Default_Aspect (Id : E) return B; - function Has_Default_Init_Cond (Id : E) return B; function Has_Delayed_Aspects (Id : E) return B; function Has_Delayed_Freeze (Id : E) return B; function Has_Delayed_Rep_Aspects (Id : E) return B; + function Has_DIC (Id : E) return B; function Has_Discriminants (Id : E) return B; function Has_Dispatch_Table (Id : E) return B; function Has_Dynamic_Predicate_Aspect (Id : E) return B; @@ -6999,7 +7004,7 @@ package Einfo is function Has_Implicit_Dereference (Id : E) return B; 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_DIC (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; @@ -7013,6 +7018,7 @@ package Einfo is 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_DIC (Id : E) return B; function Has_Own_Invariants (Id : E) return B; function Has_Partial_Visible_Refinement (Id : E) return B; function Has_Per_Object_Constraint (Id : E) return B; @@ -7098,8 +7104,8 @@ package Einfo is function Is_Controlled (Id : E) return B; function Is_Controlling_Formal (Id : E) return B; function Is_CPP_Class (Id : E) return B; - function Is_Default_Init_Cond_Procedure (Id : E) return B; function Is_Descendant_Of_Address (Id : E) return B; + function Is_DIC_Procedure (Id : E) return B; function Is_Discrim_SO_Function (Id : E) return B; function Is_Discriminant_Check_Function (Id : E) return B; function Is_Dispatch_Table_Entity (Id : E) return B; @@ -7664,7 +7670,6 @@ package Einfo is procedure Set_Has_Controlling_Result (Id : E; V : B := True); procedure Set_Has_Convention_Pragma (Id : E; V : B := True); procedure Set_Has_Default_Aspect (Id : E; V : B := True); - procedure Set_Has_Default_Init_Cond (Id : E; V : B := True); procedure Set_Has_Delayed_Aspects (Id : E; V : B := True); procedure Set_Has_Delayed_Freeze (Id : E; V : B := True); procedure Set_Has_Delayed_Rep_Aspects (Id : E; V : B := True); @@ -7681,7 +7686,7 @@ package Einfo is procedure Set_Has_Implicit_Dereference (Id : E; V : B := True); 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_DIC (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_Loop_Entry_Attributes (Id : E; V : B := True); @@ -7693,6 +7698,7 @@ package Einfo is 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_DIC (Id : E; V : B := True); procedure Set_Has_Own_Invariants (Id : E; V : B := True); procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True); procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True); @@ -7778,8 +7784,8 @@ package Einfo is procedure Set_Is_Controlled (Id : E; V : B := True); procedure Set_Is_Controlling_Formal (Id : E; V : B := True); procedure Set_Is_CPP_Class (Id : E; V : B := True); - procedure Set_Is_Default_Init_Cond_Procedure (Id : E; V : B := True); procedure Set_Is_Descendant_Of_Address (Id : E; V : B := True); + procedure Set_Is_DIC_Procedure (Id : E; V : B := True); procedure Set_Is_Discrim_SO_Function (Id : E; V : B := True); procedure Set_Is_Discriminant_Check_Function (Id : E; V : B := True); procedure Set_Is_Dispatch_Table_Entity (Id : E; V : B := True); @@ -8009,17 +8015,17 @@ package Einfo is -- Access to Subprograms in Subprograms_For_Type -- --------------------------------------------------- - 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; + function DIC_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); + procedure Set_DIC_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); ----------------------------------- -- Field Initialization Routines -- @@ -8459,7 +8465,6 @@ package Einfo is pragma Inline (Has_Controlling_Result); pragma Inline (Has_Convention_Pragma); pragma Inline (Has_Default_Aspect); - pragma Inline (Has_Default_Init_Cond); pragma Inline (Has_Delayed_Aspects); pragma Inline (Has_Delayed_Freeze); pragma Inline (Has_Delayed_Rep_Aspects); @@ -8476,7 +8481,7 @@ package Einfo is pragma Inline (Has_Implicit_Dereference); pragma Inline (Has_Independent_Components); pragma Inline (Has_Inheritable_Invariants); - pragma Inline (Has_Inherited_Default_Init_Cond); + pragma Inline (Has_Inherited_DIC); pragma Inline (Has_Inherited_Invariants); pragma Inline (Has_Initial_Value); pragma Inline (Has_Loop_Entry_Attributes); @@ -8488,6 +8493,7 @@ package Einfo is pragma Inline (Has_Non_Standard_Rep); pragma Inline (Has_Object_Size_Clause); pragma Inline (Has_Out_Or_In_Out_Parameter); + pragma Inline (Has_Own_DIC); pragma Inline (Has_Own_Invariants); pragma Inline (Has_Partial_Visible_Refinement); pragma Inline (Has_Per_Object_Constraint); @@ -8584,8 +8590,8 @@ package Einfo is pragma Inline (Is_Controlling_Formal); pragma Inline (Is_CPP_Class); pragma Inline (Is_Decimal_Fixed_Point_Type); - pragma Inline (Is_Default_Init_Cond_Procedure); pragma Inline (Is_Descendant_Of_Address); + pragma Inline (Is_DIC_Procedure); pragma Inline (Is_Digits_Type); pragma Inline (Is_Discrete_Or_Fixed_Point_Type); pragma Inline (Is_Discrete_Type); @@ -8978,7 +8984,6 @@ package Einfo is pragma Inline (Set_Has_Controlling_Result); pragma Inline (Set_Has_Convention_Pragma); pragma Inline (Set_Has_Default_Aspect); - pragma Inline (Set_Has_Default_Init_Cond); pragma Inline (Set_Has_Delayed_Aspects); pragma Inline (Set_Has_Delayed_Freeze); pragma Inline (Set_Has_Delayed_Rep_Aspects); @@ -8995,7 +9000,7 @@ package Einfo is pragma Inline (Set_Has_Implicit_Dereference); 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_DIC); pragma Inline (Set_Has_Inherited_Invariants); pragma Inline (Set_Has_Initial_Value); pragma Inline (Set_Has_Loop_Entry_Attributes); @@ -9007,6 +9012,7 @@ package Einfo is 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_DIC); pragma Inline (Set_Has_Own_Invariants); pragma Inline (Set_Has_Partial_Visible_Refinement); pragma Inline (Set_Has_Per_Object_Constraint); @@ -9090,8 +9096,8 @@ package Einfo is pragma Inline (Set_Is_Controlled); pragma Inline (Set_Is_Controlling_Formal); pragma Inline (Set_Is_CPP_Class); - pragma Inline (Set_Is_Default_Init_Cond_Procedure); pragma Inline (Set_Is_Descendant_Of_Address); + pragma Inline (Set_Is_DIC_Procedure); pragma Inline (Set_Is_Discrim_SO_Function); pragma Inline (Set_Is_Discriminant_Check_Function); pragma Inline (Set_Is_Dispatch_Table_Entity); diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index cd349dbd..bee99ca 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -6528,19 +6528,18 @@ package body Exp_Ch3 is -- pragma Default_Initial_Condition, add a runtime check to verify -- the assumption of the pragma (SPARK RM 7.3.3). Generate: - -- <Base_Typ>Default_Init_Cond (<Base_Typ> (Def_Id)); + -- <Base_Typ>DIC (<Base_Typ> (Def_Id)); -- Note that the check is generated for source objects only if Comes_From_Source (Def_Id) - and then (Has_Default_Init_Cond (Typ) - or else Has_Inherited_Default_Init_Cond (Typ)) + and then Has_DIC (Typ) + and then Present (DIC_Procedure (Typ)) and then not Has_Init_Expression (N) - and then Present (Default_Init_Cond_Procedure (Typ)) then declare - DIC_Call : constant Node_Id := - Build_Default_Init_Cond_Call (Loc, Def_Id, Typ); + DIC_Call : constant Node_Id := Build_DIC_Call (Loc, Def_Id, Typ); + begin if Present (Next_N) then Insert_Before_And_Analyze (Next_N, DIC_Call); @@ -7320,6 +7319,13 @@ package body Exp_Ch3 is Process_Pending_Access_Types (Def_Id); Freeze_Stream_Operations (N, Def_Id); + -- Generate the [spec and] body of the procedure tasked with the runtime + -- verification of pragma Default_Initial_Condition's expression. + + if Has_DIC (Def_Id) then + Build_DIC_Procedure_Body (Def_Id); + end if; + -- 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 diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index ac188b4..7f49f32 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -3525,9 +3525,6 @@ package body Exp_Ch7 is -- 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; @@ -3589,7 +3586,7 @@ package body Exp_Ch7 is -- effect. if not Has_Null_Body (Proc_Id) then - Create_Append (Comp_Checks, + Append_New_To (Comp_Checks, Make_Procedure_Call_Statement (Loc, Name => New_Occurrence_Of (Proc_Id, Loc), @@ -3628,7 +3625,7 @@ package body Exp_Ch7 is -- effect. if not Has_Null_Body (Proc_Id) then - Create_Append (Comp_Checks, + Append_New_To (Comp_Checks, Make_If_Statement (Loc, Condition => Make_Op_Ne (Loc, @@ -3703,7 +3700,7 @@ package body Exp_Ch7 is -- effect. if Present (Comp_Checks) then - Create_Append (Dim_Checks, + Append_New_To (Dim_Checks, Make_Implicit_Loop_Statement (T, Identifier => Empty, Iteration_Scheme => @@ -3906,7 +3903,7 @@ package body Exp_Ch7 is Var_Stmts := New_List (Make_Null_Statement (Loc)); end if; - Create_Append (Var_Alts, + Append_New_To (Var_Alts, Make_Case_Statement_Alternative (Loc, Discrete_Choices => New_Copy_List (Discrete_Choices (Var)), @@ -3920,7 +3917,7 @@ package body Exp_Ch7 is -- values only when there is at least one real invariant check. if Produced_Variant_Check then - Create_Append (CL_Checks, + Append_New_To (CL_Checks, Make_Case_Statement (Loc, Expression => Make_Selected_Component (Loc, @@ -3980,7 +3977,7 @@ package body Exp_Ch7 is -- effect. if not Has_Null_Body (Proc_Id) then - Create_Append (Comp_Checks, + Append_New_To (Comp_Checks, Make_Procedure_Call_Statement (Loc, Name => New_Occurrence_Of (Proc_Id, Loc), @@ -4023,7 +4020,7 @@ package body Exp_Ch7 is -- effect. if not Has_Null_Body (Proc_Id) then - Create_Append (Comp_Checks, + Append_New_To (Comp_Checks, Make_If_Statement (Loc, Condition => Make_Op_Ne (Loc, @@ -4356,7 +4353,7 @@ package body Exp_Ch7 is -- Generate: -- pragma Check (<Nam>, <Expr>, <Str>); - Create_Append (Checks, + Append_New_To (Checks, Make_Pragma (Ploc, Chars => Name_Check, Pragma_Argument_Associations => Assoc)); @@ -4443,19 +4440,6 @@ package body Exp_Ch7 is 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 -- ------------------------------------ @@ -4494,11 +4478,6 @@ package body Exp_Ch7 is 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 @@ -4539,10 +4518,15 @@ package body Exp_Ch7 is pragma Assert (Has_Invariants (Work_Typ)); + -- ??? invariants of class-wide types are not properly implemented + + if Is_Class_Wide_Type (Work_Typ) then + return; + -- Nothing to do for interface types as their class-wide invariants are -- inherited by implementing types. - if Is_Interface (Work_Typ) then + elsif Is_Interface (Work_Typ) then return; end if; @@ -4633,7 +4617,6 @@ package body Exp_Ch7 is if Partial_Invariant then pragma Assert (Present (Priv_Typ)); - Freeze_Typ := Priv_Typ; Add_Type_Invariants (Priv_Typ => Priv_Typ, @@ -4650,7 +4633,6 @@ package body Exp_Ch7 is else pragma Assert (Present (Full_Typ)); - Freeze_Typ := Full_Typ; -- Check the invariants of the partial view by calling the "partial" -- invariant procedure. Generate: @@ -4658,7 +4640,7 @@ package body Exp_Ch7 is -- <Work_Typ>Partial_Invariant (_object); if Present (Part_Proc) then - Create_Append (Stmts, + Append_New_To (Stmts, Make_Procedure_Call_Statement (Loc, Name => New_Occurrence_Of (Part_Proc, Loc), Parameter_Associations => New_List ( @@ -4793,7 +4775,7 @@ package body Exp_Ch7 is -- Otherwise the body is part of the freezing actions of the type else - Append_Freeze_Action (Freeze_Typ, Proc_Body); + Append_Freeze_Action (Work_Typ, Proc_Body); end if; Ghost_Mode := Save_Ghost_Mode; @@ -4860,10 +4842,15 @@ package body Exp_Ch7 is pragma Assert (Has_Invariants (Work_Typ)); + -- ??? invariants of class-wide types are not properly implemented + + if Is_Class_Wide_Type (Work_Typ) then + return; + -- Nothing to do for interface types as their class-wide invariants are -- inherited by implementing types. - if Is_Interface (Work_Typ) then + elsif Is_Interface (Work_Typ) then return; -- Nothing to do if the type already has a "partial" invariant procedure diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 31eaf6e..1529c56 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -46,8 +46,12 @@ with Restrict; use Restrict; with Rident; use Rident; with Sem; use Sem; with Sem_Aux; use Sem_Aux; +with Sem_Ch3; use Sem_Ch3; +with Sem_Ch6; use Sem_Ch6; with Sem_Ch8; use Sem_Ch8; +with Sem_Ch12; use Sem_Ch12; with Sem_Ch13; use Sem_Ch13; +with Sem_Disp; use Sem_Disp; with Sem_Eval; use Sem_Eval; with Sem_Res; use Sem_Res; with Sem_Type; use Sem_Type; @@ -61,8 +65,46 @@ with Ttypes; use Ttypes; with Urealp; use Urealp; with Validsw; use Validsw; +with GNAT.HTable; use GNAT.HTable; + package body Exp_Util is + --------------------------------------------------------- + -- Handling of inherited class-wide pre/postconditions -- + --------------------------------------------------------- + + -- Following AI12-0113, the expression for a class-wide condition is + -- transformed for a subprogram that inherits it, by replacing calls + -- to primitive operations of the original controlling type into the + -- corresponding overriding operations of the derived type. The following + -- hash table manages this mapping, and is expanded on demand whenever + -- such inherited expression needs to be constructed. + + -- The mapping is also used to check whether an inherited operation has + -- a condition that depends on overridden operations. For such an + -- operation we must create a wrapper that is then treated as a normal + -- overriding. In SPARK mode such operations are illegal. + + -- For a given root type there may be several type extensions with their + -- own overriding operations, so at various times a given operation of + -- the root will be mapped into different overridings. The root type is + -- also mapped into the current type extension to indicate that its + -- operations are mapped into the overriding operations of that current + -- type extension. + + Primitives_Mapping_Size : constant := 511; + + subtype Num_Primitives is Integer range 0 .. Primitives_Mapping_Size - 1; + function Entity_Hash (E : Entity_Id) return Num_Primitives; + + package Primitives_Mapping is new GNAT.HTable.Simple_HTable + (Header_Num => Num_Primitives, + Key => Entity_Id, + Element => Entity_Id, + No_element => Empty, + Hash => Entity_Hash, + Equal => "="); + ----------------------- -- Local Subprograms -- ----------------------- @@ -113,6 +155,11 @@ package body Exp_Util is -- Force evaluation of bounds of a slice, which may be given by a range -- or by a subtype indication with or without a constraint. + function Find_DIC_Type (Typ : Entity_Id) return Entity_Id; + -- Subsidiary to all Build_DIC_Procedure_xxx routines. Find the type which + -- defines the Default_Initial_Condition pragma of type Typ. This is either + -- Typ itself or a parent type when the pragma is inherited. + function Make_CW_Equivalent_Type (T : Entity_Id; E : Node_Id) return Entity_Id; @@ -984,6 +1031,1074 @@ package body Exp_Util is return Blk; end Build_Abort_Undefer_Block; + --------------------------------- + -- Build_Class_Wide_Expression -- + --------------------------------- + + procedure Build_Class_Wide_Expression + (Prag : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id; + Adjust_Sloc : Boolean) + is + function Replace_Entity (N : Node_Id) return Traverse_Result; + -- Replace reference to formal of inherited operation or to primitive + -- operation of root type, with corresponding entity for derived type, + -- when constructing the class-wide condition of an overriding + -- subprogram. + + -------------------- + -- Replace_Entity -- + -------------------- + + function Replace_Entity (N : Node_Id) return Traverse_Result is + New_E : Entity_Id; + + begin + if Adjust_Sloc then + Adjust_Inherited_Pragma_Sloc (N); + end if; + + if Nkind (N) = N_Identifier + and then Present (Entity (N)) + and then + (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N))) + and then + (Nkind (Parent (N)) /= N_Attribute_Reference + or else Attribute_Name (Parent (N)) /= Name_Class) + then + -- The replacement does not apply to dispatching calls within the + -- condition, but only to calls whose static tag is that of the + -- parent type. + + if Is_Subprogram (Entity (N)) + and then Nkind (Parent (N)) = N_Function_Call + and then Present (Controlling_Argument (Parent (N))) + then + return OK; + end if; + + -- Determine whether entity has a renaming + + New_E := Primitives_Mapping.Get (Entity (N)); + + if Present (New_E) then + Rewrite (N, New_Occurrence_Of (New_E, Sloc (N))); + end if; + + -- Check that there are no calls left to abstract operations if + -- the current subprogram is not abstract. + + if Nkind (Parent (N)) = N_Function_Call + and then N = Name (Parent (N)) + then + if not Is_Abstract_Subprogram (Subp) + and then Is_Abstract_Subprogram (Entity (N)) + then + Error_Msg_Sloc := Sloc (Current_Scope); + Error_Msg_NE + ("cannot call abstract subprogram in inherited condition " + & "for&#", N, Current_Scope); + + -- In SPARK mode, reject an inherited condition for an + -- inherited operation if it contains a call to an overriding + -- operation, because this implies that the pre/postcondition + -- of the inherited operation have changed silently. + + elsif SPARK_Mode = On + and then Warn_On_Suspicious_Contract + and then Present (Alias (Subp)) + and then Present (New_E) + and then Comes_From_Source (New_E) + then + Error_Msg_N + ("cannot modify inherited condition (SPARK RM 6.1.1(1))", + Parent (Subp)); + Error_Msg_Sloc := Sloc (New_E); + Error_Msg_Node_2 := Subp; + Error_Msg_NE + ("\overriding of&# forces overriding of&", + Parent (Subp), New_E); + end if; + end if; + + -- Update type of function call node, which should be the same as + -- the function's return type. + + if Is_Subprogram (Entity (N)) + and then Nkind (Parent (N)) = N_Function_Call + then + Set_Etype (Parent (N), Etype (Entity (N))); + end if; + + -- The whole expression will be reanalyzed + + elsif Nkind (N) in N_Has_Etype then + Set_Analyzed (N, False); + end if; + + return OK; + end Replace_Entity; + + procedure Replace_Condition_Entities is + new Traverse_Proc (Replace_Entity); + + -- Local variables + + Par_Formal : Entity_Id; + Subp_Formal : Entity_Id; + + -- Start of processing for Build_Class_Wide_Expression + + begin + -- Add mapping from old formals to new formals + + Par_Formal := First_Formal (Par_Subp); + Subp_Formal := First_Formal (Subp); + + while Present (Par_Formal) and then Present (Subp_Formal) loop + Primitives_Mapping.Set (Par_Formal, Subp_Formal); + Next_Formal (Par_Formal); + Next_Formal (Subp_Formal); + end loop; + + Replace_Condition_Entities (Prag); + end Build_Class_Wide_Expression; + + -------------------- + -- Build_DIC_Call -- + -------------------- + + function Build_DIC_Call + (Loc : Source_Ptr; + Obj_Id : Entity_Id; + Typ : Entity_Id) return Node_Id + is + Proc_Id : constant Entity_Id := DIC_Procedure (Typ); + Formal_Typ : constant Entity_Id := Etype (First_Formal (Proc_Id)); + + begin + return + Make_Procedure_Call_Statement (Loc, + Name => New_Occurrence_Of (Proc_Id, Loc), + Parameter_Associations => New_List ( + Make_Unchecked_Type_Conversion (Loc, + Subtype_Mark => New_Occurrence_Of (Formal_Typ, Loc), + Expression => New_Occurrence_Of (Obj_Id, Loc)))); + end Build_DIC_Call; + + ------------------------------ + -- Build_DIC_Procedure_Body -- + ------------------------------ + + procedure Build_DIC_Procedure_Body (Typ : Entity_Id) is + procedure Add_DIC_Check + (DIC_Prag : Node_Id; + DIC_Expr : Node_Id; + Stmts : in out List_Id); + -- Subsidiary to all Add_xxx_DIC routines. Add a runtime check to verify + -- assertion expression DIC_Expr of pragma DIC_Prag. All generated code + -- is added to list Stmts. + + procedure Add_Inherited_DIC + (DIC_Prag : Node_Id; + Par_Typ : Entity_Id; + Deriv_Typ : Entity_Id; + Stmts : in out List_Id); + -- Add a runtime check to verify the assertion expression of inherited + -- pragma DIC_Prag. Par_Typ is parent type which is also the owner of + -- the DIC pragma. Deriv_Typ is the derived type inheriting the DIC + -- pragma. All generated code is added to list Stmts. + + procedure Add_Inherited_Tagged_DIC + (DIC_Prag : Node_Id; + Par_Typ : Entity_Id; + Deriv_Typ : Entity_Id; + Stmts : in out List_Id); + -- Add a runtime check to verify assertion expression DIC_Expr of + -- inherited pragma DIC_Prag. This routine applies class-wide pre- and + -- postcondition-like runtime semantics to the check. Par_Typ is the + -- parent type whose DIC pragma is being inherited. Deriv_Typ is the + -- derived type inheriting the DIC pragma. All generated code is added + -- to list Stmts. + + procedure Add_Own_DIC + (DIC_Prag : Node_Id; + DIC_Typ : Entity_Id; + Stmts : in out List_Id); + -- Add a runtime check to verify the assertion expression of pragma + -- DIC_Prag. DIC_Typ is the owner of the DIC pragma. All generated code + -- is added to list Stmts. + + procedure Replace_Object_And_Primitive_References + (Expr : Node_Id; + Par_Typ : Entity_Id; + Deriv_Typ : Entity_Id); + -- Expr denotes an arbitrary expression. Par_Typ is a parent type in a + -- type hierarchy. Deriv_Typ is a type derived from Par_Typ. Perform the + -- following substitutions: + -- + -- * Replace a reference to the _object parameter of the parent type's + -- DIC procedure with a reference to the _object parameter of the + -- derived type's DIC procedure. + -- + -- * 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. + + procedure Replace_Type_References + (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. + + ------------------- + -- Add_DIC_Check -- + ------------------- + + procedure Add_DIC_Check + (DIC_Prag : Node_Id; + DIC_Expr : Node_Id; + Stmts : in out List_Id) + is + Loc : constant Source_Ptr := Sloc (DIC_Prag); + Nam : constant Name_Id := Original_Aspect_Pragma_Name (DIC_Prag); + + begin + -- The DIC pragma is ignored, nothing left to do + + if Is_Ignored (DIC_Prag) then + null; + + -- Otherwise the DIC expression must be checked at runtime. Generate: + + -- pragma Check (<Nam>, <DIC_Expr>); + + else + Append_New_To (Stmts, + Make_Pragma (Loc, + Pragma_Identifier => + Make_Identifier (Loc, Name_Check), + + Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Nam)), + + Make_Pragma_Argument_Association (Loc, + Expression => DIC_Expr)))); + end if; + end Add_DIC_Check; + + ----------------------- + -- Add_Inherited_DIC -- + ----------------------- + + procedure Add_Inherited_DIC + (DIC_Prag : Node_Id; + Par_Typ : Entity_Id; + Deriv_Typ : Entity_Id; + Stmts : in out List_Id) + is + Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ); + Deriv_Obj : constant Entity_Id := First_Entity (Deriv_Proc); + Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ); + Par_Obj : constant Entity_Id := First_Entity (Par_Proc); + Loc : constant Source_Ptr := Sloc (DIC_Prag); + + begin + pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc)); + + -- Verify the inherited DIC assertion expression by calling the DIC + -- procedure of the parent type. + + -- Generate: + -- <Par_Typ>DIC (Par_Typ (_object)); + + Append_New_To (Stmts, + Make_Procedure_Call_Statement (Loc, + Name => New_Occurrence_Of (Par_Proc, Loc), + Parameter_Associations => New_List ( + Convert_To + (Typ => Etype (Par_Obj), + Expr => New_Occurrence_Of (Deriv_Obj, Loc))))); + end Add_Inherited_DIC; + + ------------------------------ + -- Add_Inherited_Tagged_DIC -- + ------------------------------ + + procedure Add_Inherited_Tagged_DIC + (DIC_Prag : Node_Id; + Par_Typ : Entity_Id; + Deriv_Typ : Entity_Id; + Stmts : in out List_Id) + is + DIC_Args : constant List_Id := + Pragma_Argument_Associations (DIC_Prag); + DIC_Arg : constant Node_Id := First (DIC_Args); + DIC_Expr : constant Node_Id := Expression_Copy (DIC_Arg); + Typ_Decl : constant Node_Id := Declaration_Node (Deriv_Typ); + + Expr : Node_Id; + + begin + -- The processing of an inherited DIC assertion expression starts off + -- with a copy of the original parent expression where all references + -- to the parent type have already been replaced with references to + -- the _object formal parameter of the parent type's DIC procedure. + + pragma Assert (Present (DIC_Expr)); + Expr := New_Copy_Tree (DIC_Expr); + + -- Perform the following substitutions: + + -- * Replace a reference to the _object parameter of the parent + -- type's DIC procedure with a reference to the _object parameter + -- of the derived types' DIC procedure. + + -- * 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. + + -- Note that primitives defined in the private part are automatically + -- handled by the overriding/inheritance mechanism and do not require + -- an extra replacement pass. + + Replace_Object_And_Primitive_References + (Expr => Expr, + Par_Typ => Par_Typ, + Deriv_Typ => Deriv_Typ); + + -- Preanalyze the DIC expression to detect errors and at the same + -- time capture the visibility of the proper package part. + + Set_Parent (Expr, Typ_Decl); + Preanalyze_Assert_Expression (Expr, Any_Boolean); + + -- Once the DIC assertion expression is fully processed, add a check + -- to the statements of the DIC procedure. + + Add_DIC_Check + (DIC_Prag => DIC_Prag, + DIC_Expr => Expr, + Stmts => Stmts); + end Add_Inherited_Tagged_DIC; + + ----------------- + -- Add_Own_DIC -- + ----------------- + + procedure Add_Own_DIC + (DIC_Prag : Node_Id; + DIC_Typ : Entity_Id; + Stmts : in out List_Id) + is + DIC_Args : constant List_Id := + Pragma_Argument_Associations (DIC_Prag); + DIC_Arg : constant Node_Id := First (DIC_Args); + DIC_Asp : constant Node_Id := Corresponding_Aspect (DIC_Prag); + DIC_Expr : constant Node_Id := Get_Pragma_Arg (DIC_Arg); + DIC_Proc : constant Entity_Id := DIC_Procedure (DIC_Typ); + Obj_Id : constant Entity_Id := First_Formal (DIC_Proc); + + procedure Preanalyze_Own_DIC_For_ASIS; + -- Preanalyze the original DIC expression of an aspect or a source + -- pragma for ASIS. + + --------------------------------- + -- Preanalyze_Own_DIC_For_ASIS -- + --------------------------------- + + procedure Preanalyze_Own_DIC_For_ASIS is + Expr : Node_Id := Empty; + + begin + -- The DIC pragma is a source construct, preanalyze the original + -- expression of the pragma. + + if Comes_From_Source (DIC_Prag) then + Expr := DIC_Expr; + + -- Otherwise preanalyze the expression of the corresponding aspect + + elsif Present (DIC_Asp) then + Expr := Expression (DIC_Asp); + end if; + + -- The expression must be subjected to the same substitutions as + -- the copy used in the generation of the runtime check. + + if Present (Expr) then + Replace_Type_References + (Expr => Expr, + Typ => DIC_Typ, + Obj_Id => Obj_Id); + + Preanalyze_Assert_Expression (Expr, Any_Boolean); + end if; + end Preanalyze_Own_DIC_For_ASIS; + + -- Local variables + + Typ_Decl : constant Node_Id := Declaration_Node (DIC_Typ); + + Expr : Node_Id; + + -- Start of processing for Add_Own_DIC + + begin + Expr := New_Copy_Tree (DIC_Expr); + + -- Perform the following substituion: + + -- * Replace the current instance of DIC_Typ with a reference to + -- the _object formal parameter of the DIC procedure. + + Replace_Type_References + (Expr => Expr, + Typ => DIC_Typ, + Obj_Id => Obj_Id); + + -- Preanalyze the DIC expression to detect errors and at the same + -- time capture the visibility of the proper package part. + + Set_Parent (Expr, Typ_Decl); + Preanalyze_Assert_Expression (Expr, Any_Boolean); + + -- Save a copy of the expression with all replacements and analysis + -- already taken place in case a derived type inherits the pragma. + -- The copy will be used as the foundation of the derived type's own + -- version of the DIC assertion expression. + + if Is_Tagged_Type (DIC_Typ) then + Set_Expression_Copy (DIC_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 (DIC_Asp) then + Set_Entity (Identifier (DIC_Asp), New_Copy_Tree (Expr)); + end if; + + -- Preanalyze the original DIC expression for ASIS + + if ASIS_Mode then + Preanalyze_Own_DIC_For_ASIS; + end if; + + -- Once the DIC assertion expression is fully processed, add a check + -- to the statements of the DIC procedure. + + Add_DIC_Check + (DIC_Prag => DIC_Prag, + DIC_Expr => Expr, + Stmts => Stmts); + end Add_Own_DIC; + + --------------------------------------------- + -- Replace_Object_And_Primitive_References -- + --------------------------------------------- + + procedure Replace_Object_And_Primitive_References + (Expr : Node_Id; + Par_Typ : Entity_Id; + Deriv_Typ : Entity_Id) + is + Deriv_Obj : Entity_Id; + -- The _object parameter of the derived type's DIC procedure + + Par_Obj : Entity_Id; + -- The _object parameter of the parent type's DIC procedure + + function Replace_Ref (Ref : Node_Id) return Traverse_Result; + -- Substitute a reference to an entity with a reference to the + -- corresponding entity stored in in table Primitives_Mapping. + + ----------------- + -- Replace_Ref -- + ----------------- + + function Replace_Ref (Ref : Node_Id) return Traverse_Result is + Context : constant Node_Id := Parent (Ref); + Loc : constant Source_Ptr := Sloc (Ref); + New_Id : Entity_Id; + New_Ref : Node_Id; + Ref_Id : Entity_Id; + Result : Traverse_Result; + + begin + Result := OK; + + -- The current node denotes a reference + + if Nkind (Ref) in N_Has_Entity and then Present (Entity (Ref)) then + Ref_Id := Entity (Ref); + New_Id := Primitives_Mapping.Get (Ref_Id); + + -- The reference mentions a parent type primitive which has a + -- corresponding derived type primitive. + + if Present (New_Id) then + New_Ref := New_Occurrence_Of (New_Id, Loc); + + -- The reference mentions the _object parameter of the parent + -- type's DIC procedure. + + elsif Ref_Id = Par_Obj then + New_Ref := New_Occurrence_Of (Deriv_Obj, Loc); + + -- The reference to _object acts as an actual parameter in a + -- subprogram call which may be invoking a primitive of the + -- parent type: + + -- Primitive (... _object ...); + + -- The parent type primitive may not be overridden nor + -- inherited when it is declared after the derived type + -- definition: + + -- type Parent is tagged private; + -- type Child is new Parent with private; + -- procedure Primitive (Obj : Parent); + + -- In this scenario the _object parameter is converted to + -- the parent type. + + if Nkind_In (Context, N_Function_Call, + N_Procedure_Call_Statement) + and then + No (Primitives_Mapping.Get (Entity (Name (Context)))) + then + New_Ref := Convert_To (Par_Typ, New_Ref); + + -- Do not process the generated type conversion because + -- both the parent type and the derived type are in the + -- Primitives_Mapping table. This will clobber the type + -- conversion by resetting its subtype mark. + + Result := Skip; + end if; + + -- Otherwise there is nothing to replace + + else + New_Ref := Empty; + end if; + + if Present (New_Ref) then + Rewrite (Ref, New_Ref); + + -- Update the return type when the context of the reference + -- acts as the name of a function call. Note that the update + -- should not be performed when the reference appears as an + -- actual in the call. + + if Nkind (Context) = N_Function_Call + and then Name (Context) = Ref + then + Set_Etype (Context, Etype (New_Id)); + end if; + end if; + end if; + + -- Reanalyze the reference due to potential replacements + + if Nkind (Ref) in N_Has_Etype then + Set_Analyzed (Ref, False); + end if; + + return Result; + end Replace_Ref; + + procedure Replace_Refs is new Traverse_Proc (Replace_Ref); + + -- Local variables + + Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ); + Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ); + + -- Start of processing for Replace_Object_And_Primitive_References + + begin + pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc)); + + Deriv_Obj := First_Entity (Deriv_Proc); + Par_Obj := First_Entity (Par_Proc); + + -- Map each primitive operation of the parent type to the proper + -- primitive of the derived type. + + Update_Primitives_Mapping_Of_Types + (Par_Typ => Par_Typ, + Deriv_Typ => Deriv_Typ); + + -- Inspect the input expression and perform substitutions where + -- necessary. + + Replace_Refs (Expr); + end Replace_Object_And_Primitive_References; + + ----------------------------- + -- Replace_Type_References -- + ----------------------------- + + procedure Replace_Type_References + (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 + -- with a reference to Obj_Id. + + ---------------------- + -- Replace_Type_Ref -- + ---------------------- + + procedure Replace_Type_Ref (N : Node_Id) is + Ref : Node_Id; + + begin + -- Decorate the reference to 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, Typ); + Set_Etype (N, Typ); + + elsif Nkind (N) = N_Selected_Component then + Analyze (Prefix (N)); + Set_Entity (Selector_Name (N), Typ); + Set_Etype (Selector_Name (N), Typ); + end if; + + -- Perform the following substitution: + + -- Typ --> _object + + Ref := Make_Identifier (Sloc (N), Chars (Obj_Id)); + Set_Entity (Ref, Obj_Id); + Set_Etype (Ref, Typ); + + Rewrite (N, Ref); + + Set_Comes_From_Source (N, True); + end Replace_Type_Ref; + + procedure Replace_Type_Refs is + new Replace_Type_References_Generic (Replace_Type_Ref); + + -- Start of processing for Replace_Type_References + + begin + Replace_Type_Refs (Expr, Typ); + end Replace_Type_References; + + -- Local variables + + Loc : constant Source_Ptr := Sloc (Typ); + + Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + + DIC_Prag : Node_Id; + DIC_Typ : Entity_Id; + Dummy_1 : Entity_Id; + Dummy_2 : Entity_Id; + Proc_Body : Node_Id; + Proc_Body_Id : Entity_Id; + Proc_Decl : Node_Id; + Proc_Id : Entity_Id; + Stmts : List_Id := No_List; + + Work_Typ : Entity_Id; + -- The working type + + -- Start of processing for Build_DIC_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 the DIC pragma is 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 working type must be either define a DIC pragma of its own or + -- inherit one from a parent type. + + pragma Assert (Has_DIC (Work_Typ)); + + -- Recover the type which defines the DIC pragma. This is either the + -- working type itself or a parent type when the pragma is inherited. + + DIC_Typ := Find_DIC_Type (Work_Typ); + pragma Assert (Present (DIC_Typ)); + + DIC_Prag := Get_Pragma (DIC_Typ, Pragma_Default_Initial_Condition); + pragma Assert (Present (DIC_Prag)); + + -- Nothing to do if pragma DIC appears without an argument or its sole + -- argument is "null". + + if not Is_Verifiable_DIC_Pragma (DIC_Prag) then + return; + end if; + + -- The working type may lack a DIC procedure declaration. This may be + -- due to several reasons: + + -- * The working type's own DIC pragma does not contain a verifiable + -- assertion expression. In this case there is no need to build a + -- DIC procedure because there is nothing to check. + + -- * The working type derives from a parent type. In this case a DIC + -- procedure should be built only when the inherited DIC pragma has + -- a verifiable assertion expression. + + Proc_Id := DIC_Procedure (Work_Typ); + + -- Build a DIC procedure declaration when the working type derives from + -- a parent type. + + if No (Proc_Id) then + Build_DIC_Procedure_Declaration (Work_Typ); + Proc_Id := DIC_Procedure (Work_Typ); + end if; + + -- At this point there should be a DIC procedure declaration + + pragma Assert (Present (Proc_Id)); + Proc_Decl := Unit_Declaration_Node (Proc_Id); + + -- Nothing to do if the DIC 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 DIC procedure is properly marked as Ghost. + + Set_Ghost_Mode_From_Entity (Work_Typ); + + -- Emulate the environment of the DIC procedure by installing its scope + -- and formal parameters. + + Push_Scope (Proc_Id); + Install_Formals (Proc_Id); + + -- The working type defines its own DIC pragma. Replace the current + -- instance of the working type with the formal of the DIC procedure. + -- Note that there is no need to consider inherited DIC pragmas from + -- parent types because the working type's DIC pragma "hides" all + -- inherited DIC pragmas. + + if Has_Own_DIC (Work_Typ) then + pragma Assert (DIC_Typ = Work_Typ); + + Add_Own_DIC + (DIC_Prag => DIC_Prag, + DIC_Typ => DIC_Typ, + Stmts => Stmts); + + -- Otherwise the working type inherits a DIC pragma from a parent type + + else + pragma Assert (Has_Inherited_DIC (Work_Typ)); + pragma Assert (DIC_Typ /= Work_Typ); + + -- The working type is tagged. The verification of the assertion + -- expression is subject to the same semantics as class-wide pre- + -- and postconditions. + + if Is_Tagged_Type (Work_Typ) then + Add_Inherited_Tagged_DIC + (DIC_Prag => DIC_Prag, + Par_Typ => DIC_Typ, + Deriv_Typ => Work_Typ, + Stmts => Stmts); + + -- Otherwise the working type is not tagged. Verify the assertion + -- expression of the inherited DIC pragma by directly calling the + -- DIC procedure of the parent type. + + else + Add_Inherited_DIC + (DIC_Prag => DIC_Prag, + Par_Typ => DIC_Typ, + Deriv_Typ => Work_Typ, + Stmts => Stmts); + end if; + end if; + + End_Scope; + + -- Produce an empty completing body in the following cases: + -- * Assertions are disabled + -- * The DIC Assertion_Policy is Ignore + -- * Pragma DIC appears without an argument + -- * Pragma DIC appears with argument "null" + + if No (Stmts) then + Stmts := New_List (Make_Null_Statement (Loc)); + end if; + + -- Generate: + -- procedure <Work_Typ>DIC (_object : <Work_Typ>) is + -- begin + -- <Stmts> + -- end <Work_Typ>DIC; + + 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); + + -- Perform minor decoration in case the body is not analyzed + + Set_Ekind (Proc_Body_Id, E_Subprogram_Body); + Set_Etype (Proc_Body_Id, Standard_Void_Type); + Set_Scope (Proc_Body_Id, Current_Scope); + + -- Link both spec and body to avoid generating duplicates + + Set_Corresponding_Body (Proc_Decl, Proc_Body_Id); + Set_Corresponding_Spec (Proc_Body, Proc_Id); + + -- The body should not be inserted into the tree when the context is + -- ASIS, GNATprove or a generic unit because it is not part of the + -- template. Note that the body must still be generated in order to + -- resolve the DIC assertion expression. + + if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then + null; + + -- Otherwise the body is part of the freezing actions of the working + -- type. + + else + Append_Freeze_Action (Work_Typ, Proc_Body); + end if; + + Ghost_Mode := Save_Ghost_Mode; + end Build_DIC_Procedure_Body; + + ------------------------------------- + -- Build_DIC_Procedure_Declaration -- + ------------------------------------- + + procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is + Loc : constant Source_Ptr := Sloc (Typ); + + Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + + DIC_Prag : Node_Id; + DIC_Typ : Entity_Id; + Proc_Decl : Node_Id; + 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 DIC 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 the DIC pragma is 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 be either subject to a DIC pragma or inherit one from a + -- parent type. + + pragma Assert (Has_DIC (Work_Typ)); + + -- Recover the type which defines the DIC pragma. This is either the + -- working type itself or a parent type when the pragma is inherited. + + DIC_Typ := Find_DIC_Type (Work_Typ); + pragma Assert (Present (DIC_Typ)); + + DIC_Prag := Get_Pragma (DIC_Typ, Pragma_Default_Initial_Condition); + pragma Assert (Present (DIC_Prag)); + + -- Nothing to do if pragma DIC appears without an argument or its sole + -- argument is "null". + + if not Is_Verifiable_DIC_Pragma (DIC_Prag) then + return; + + -- Nothing to do if the type already has a DIC procedure + + elsif Present (DIC_Procedure (Work_Typ)) then + return; + end if; + + -- The working type may be subject to pragma Ghost. Set the mode now to + -- ensure that the DIC procedure is properly marked as Ghost. + + Set_Ghost_Mode_From_Entity (Work_Typ); + + Proc_Id := + Make_Defining_Identifier (Loc, + Chars => + New_External_Name (Chars (Work_Typ), "Default_Initial_Condition")); + + -- Perform minor decoration in case the declaration is not analyzed + + Set_Ekind (Proc_Id, E_Procedure); + Set_Etype (Proc_Id, Standard_Void_Type); + Set_Scope (Proc_Id, Current_Scope); + + Set_Is_DIC_Procedure (Proc_Id); + Set_DIC_Procedure (Work_Typ, Proc_Id); + + -- The DIC procedure requires debug info when the assertion expression + -- is subject to Source Coverage Obligations. + + if Opt.Generate_SCO then + Set_Needs_Debug_Info (Proc_Id); + end if; + + -- Mark the DIC 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 DIC procedure and various relevant flags with all views + + Propagate_DIC_Attributes (Priv_Typ, From_Typ => Work_Typ); + Propagate_DIC_Attributes (Full_Typ, From_Typ => Work_Typ); + Propagate_DIC_Attributes (Full_Base, From_Typ => Work_Typ); + Propagate_DIC_Attributes (CRec_Typ, From_Typ => Work_Typ); + + -- The declaration of the DIC procedure must be 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 DIC 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); + + -- Perform minor decoration in case the declaration is not analyzed + + Set_Ekind (Obj_Id, E_In_Parameter); + Set_Etype (Obj_Id, Work_Typ); + Set_Scope (Obj_Id, Proc_Id); + + Set_First_Entity (Proc_Id, Obj_Id); + + -- Generate: + -- procedure <Work_Typ>DIC (_object : <Work_Typ>); + + Proc_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))))); + + -- The declaration should not be inserted into the tree when the context + -- is ASIS, GNATprove or a generic unit because it is not part of the + -- template. + + if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then + null; + + -- Otherwise insert the declaration + + else + pragma Assert (Present (Typ_Decl)); + Insert_After_And_Analyze (Typ_Decl, Proc_Decl); + end if; + + Ghost_Mode := Save_Ghost_Mode; + end Build_DIC_Procedure_Declaration; + -------------------------- -- Build_Procedure_Form -- -------------------------- @@ -2224,6 +3339,15 @@ package body Exp_Util is end if; end Ensure_Defined; + ----------------- + -- Entity_Hash -- + ----------------- + + function Entity_Hash (E : Entity_Id) return Num_Primitives is + begin + return Num_Primitives (E mod Primitives_Mapping_Size); + end Entity_Hash; + -------------------- -- Entry_Names_OK -- -------------------- @@ -2764,6 +3888,56 @@ package body Exp_Util is return TSS (Utyp, TSS_Finalize_Address); end Finalize_Address; + ------------------- + -- Find_DIC_Type -- + ------------------- + + function Find_DIC_Type (Typ : Entity_Id) return Entity_Id is + Curr_Typ : Entity_Id; + DIC_Typ : Entity_Id; + + begin + -- The input type defines its own DIC pragma, therefore it is the owner + + if Has_Own_DIC (Typ) then + DIC_Typ := Typ; + + -- Otherwise the DIC pragma is inherited from a parent type + + else + pragma Assert (Has_Inherited_DIC (Typ)); + + -- Climb the parent chain + + Curr_Typ := Typ; + loop + -- Inspect the parent type. Do not consider subtypes as they + -- inherit the DIC attributes from their base types. + + DIC_Typ := Base_Type (Etype (Curr_Typ)); + + -- Look at the full view of a private type because the type may + -- have a hidden parent introduced in the full view. + + if Is_Private_Type (DIC_Typ) + and then Present (Full_View (DIC_Typ)) + then + DIC_Typ := Full_View (DIC_Typ); + end if; + + -- Stop the climb once the nearest parent type which defines a DIC + -- pragma of its own is encountered or when the root of the parent + -- chain is reached. + + exit when Has_Own_DIC (DIC_Typ) or else Curr_Typ = DIC_Typ; + + Curr_Typ := DIC_Typ; + end loop; + end if; + + return DIC_Typ; + end Find_DIC_Type; + ------------------------ -- Find_Interface_ADT -- ------------------------ @@ -9830,6 +11004,172 @@ package body Exp_Util is end if; end Type_May_Have_Bit_Aligned_Components; + ------------------------------- + -- Update_Primitives_Mapping -- + ------------------------------- + + procedure Update_Primitives_Mapping + (Inher_Id : Entity_Id; + Subp_Id : Entity_Id) + is + begin + Update_Primitives_Mapping_Of_Types + (Par_Typ => Find_Dispatching_Type (Inher_Id), + Deriv_Typ => Find_Dispatching_Type (Subp_Id)); + end Update_Primitives_Mapping; + + ---------------------------------------- + -- Update_Primitives_Mapping_Of_Types -- + ---------------------------------------- + + procedure Update_Primitives_Mapping_Of_Types + (Par_Typ : Entity_Id; + Deriv_Typ : Entity_Id) + is + procedure Add_Primitive (Prim : Entity_Id); + -- Find a primitive in the inheritance/overriding chain starting from + -- Prim whose dispatching type is parent type Par_Typ and add a mapping + -- between the result and primitive Prim. + + ------------------- + -- Add_Primitive -- + ------------------- + + procedure Add_Primitive (Prim : Entity_Id) is + function Ancestor_Primitive (Subp : Entity_Id) return Entity_Id; + -- Return the next ancestor primitive in the inheritance/overriding + -- chain of subprogram Subp. Return Empty if no such primitive is + -- available. + + ------------------------ + -- Ancestor_Primitive -- + ------------------------ + + function Ancestor_Primitive (Subp : Entity_Id) return Entity_Id is + Inher_Prim : constant Entity_Id := Alias (Subp); + Over_Prim : constant Entity_Id := Overridden_Operation (Subp); + + begin + -- The current subprogram overrides an ancestor primitive + + if Present (Over_Prim) then + return Over_Prim; + + -- The current subprogram is an internally generated alias of an + -- inherited ancestor primitive. + + elsif Present (Inher_Prim) then + return Inher_Prim; + + -- Otherwise the current subprogram is the root of the inheritance + -- or overriding chain. + + else + return Empty; + end if; + end Ancestor_Primitive; + + -- Local variables + + Par_Prim : Entity_Id; + + -- Start of processing for Add_Primitive + + begin + -- Inspect both the inheritance chain through the Alias attribute and + -- the overriding chain through the Overridden_Operation looking for + -- an ancestor primitive with the appropriate dispatching type. + + Par_Prim := Prim; + while Present (Par_Prim) loop + exit when Find_Dispatching_Type (Par_Prim) = Par_Typ; + Par_Prim := Ancestor_Primitive (Par_Prim); + end loop; + + -- Create a mapping of the form: + + -- Parent type primitive -> derived type primitive + + if Present (Par_Prim) then + Primitives_Mapping.Set (Par_Prim, Prim); + end if; + end Add_Primitive; + + -- Local variables + + Deriv_Prim : Entity_Id; + Par_Prim : Entity_Id; + Par_Prims : Elist_Id; + Prim_Elmt : Elmt_Id; + + -- Start of processing for Update_Primitives_Mapping_Of_Types + + begin + -- Nothing to do if there are no types to work with + + if No (Par_Typ) or else No (Deriv_Typ) then + return; + + -- Nothing to do if the mapping already exists + + elsif Primitives_Mapping.Get (Par_Typ) = Deriv_Typ then + return; + end if; + + -- Create a mapping of the form: + + -- Parent type -> Derived type + + -- to prevent any subsequent attempts to produce the same relations. + + Primitives_Mapping.Set (Par_Typ, Deriv_Typ); + + -- Inspect the primitives of the derived type and determine whether they + -- relate to the primitives of the parent type. If there is a meaningful + -- relation, create a mapping of the form: + + -- Parent type primitive -> Derived type primitive + + if Present (Direct_Primitive_Operations (Deriv_Typ)) then + Prim_Elmt := First_Elmt (Direct_Primitive_Operations (Deriv_Typ)); + while Present (Prim_Elmt) loop + Deriv_Prim := Node (Prim_Elmt); + + if Is_Subprogram (Deriv_Prim) + and then Find_Dispatching_Type (Deriv_Prim) = Deriv_Typ + then + Add_Primitive (Deriv_Prim); + end if; + + Next_Elmt (Prim_Elmt); + end loop; + end if; + + -- If the parent operation is an interface operation, the overriding + -- indicator is not present. Instead, we get from the interface + -- operation the primitive of the current type that implements it. + + if Is_Interface (Par_Typ) then + Par_Prims := Collect_Primitive_Operations (Par_Typ); + + if Present (Par_Prims) then + Prim_Elmt := First_Elmt (Par_Prims); + + while Present (Prim_Elmt) loop + Par_Prim := Node (Prim_Elmt); + Deriv_Prim := + Find_Primitive_Covering_Interface (Deriv_Typ, Par_Prim); + + if Present (Deriv_Prim) then + Primitives_Mapping.Set (Par_Prim, Deriv_Prim); + end if; + + Next_Elmt (Prim_Elmt); + end loop; + end if; + end if; + end Update_Primitives_Mapping_Of_Types; + ---------------------------------- -- Within_Case_Or_If_Expression -- ---------------------------------- diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads index b82d408..d02b6b6 100644 --- a/gcc/ada/exp_util.ads +++ b/gcc/ada/exp_util.ads @@ -247,6 +247,39 @@ package Exp_Util is -- inlining of the abort undefer routine. Note that this routine does -- not install a call to Abort_Defer. + procedure Build_Class_Wide_Expression + (Prag : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id; + Adjust_Sloc : Boolean); + -- Build the expression for an inherited class-wide condition. Prag is + -- the pragma constructed from the corresponding aspect of the parent + -- subprogram, and Subp is the overriding operation and Par_Subp is + -- the overridden operation that has the condition. Adjust_Sloc is True + -- when the sloc of nodes traversed should be adjusted for the inherited + -- pragma. The routine is also called to check whether an inherited + -- operation that is not overridden but has inherited conditions need + -- a wrapper, because the inherited condition includes calls to other + -- primitives that have been overridden. In that case the first argument + -- is the expression of the original class-wide aspect. In SPARK_Mode, such + -- operation which are just inherited but have modified pre/postconditions + -- are illegal. + + function Build_DIC_Call + (Loc : Source_Ptr; + Obj_Id : Entity_Id; + Typ : Entity_Id) return Node_Id; + -- Build a call to the DIC procedure of type Typ with Obj_Id as the actual + -- parameter. + + procedure Build_DIC_Procedure_Body (Typ : Entity_Id); + -- Create the body of the procedure which verifies the assertion expression + -- of pragma Default_Initial_Condition at runtime. + + procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id); + -- Create the declaration of the procedure which verifies the assertion + -- expression of pragma Default_Initial_Condition at runtime. + procedure Build_Procedure_Form (N : Node_Id); -- Create a procedure declaration which emulates the behavior of a function -- that returns an array type, for C-compatible generation. @@ -1055,6 +1088,21 @@ package Exp_Util is -- is conservative, in that a result of False is decisive. A result of True -- means that such a component may or may not be present. + procedure Update_Primitives_Mapping + (Inher_Id : Entity_Id; + Subp_Id : Entity_Id); + -- Map primitive operations of the parent type to the corresponding + -- operations of the descendant. Note that the descendant type may not be + -- frozen yet, so we cannot use the dispatch table directly. This is called + -- when elaborating a contract for a subprogram, and when freezing a type + -- extension to verify legality rules on inherited conditions. + + procedure Update_Primitives_Mapping_Of_Types + (Par_Typ : Entity_Id; + Deriv_Typ : Entity_Id); + -- Map the primitive operations of parent type Par_Typ to the corresponding + -- primitives of derived type Deriv_Typ. + function Within_Case_Or_If_Expression (N : Node_Id) return Boolean; -- Determine whether arbitrary node N is within a case or an if expression diff --git a/gcc/ada/nlists.adb b/gcc/ada/nlists.adb index b40446a..e366786 100644 --- a/gcc/ada/nlists.adb +++ b/gcc/ada/nlists.adb @@ -203,7 +203,6 @@ package body Nlists is ----------------- procedure Append_List (List : List_Id; To : List_Id) is - procedure Append_List_Debug; pragma Inline (Append_List_Debug); -- Output debug information if Debug_Flag_N set @@ -269,6 +268,28 @@ package body Nlists is Append_List (List, To); end Append_List_To; + ---------------- + -- Append_New -- + ---------------- + + procedure Append_New (Node : Node_Or_Entity_Id; To : in out List_Id) is + begin + if No (To) then + To := New_List; + end if; + + Append (Node, To); + end Append_New; + + ------------------- + -- Append_New_To -- + ------------------- + + procedure Append_New_To (To : in out List_Id; Node : Node_Or_Entity_Id) is + begin + Append_New (Node, To); + end Append_New_To; + --------------- -- Append_To -- --------------- diff --git a/gcc/ada/nlists.ads b/gcc/ada/nlists.ads index 5950b4a..7bfeeb9 100644 --- a/gcc/ada/nlists.ads +++ b/gcc/ada/nlists.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, 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- -- @@ -229,6 +229,16 @@ package Nlists is -- An attempt to append an error node is ignored without complaint and the -- list is unchanged. + procedure Append_New (Node : Node_Or_Entity_Id; To : in out List_Id); + pragma Inline (Append_New); + -- Appends Node at the end of node list To. If To is non-existent list, a + -- list is created. Node must be a non-empty node that is not already a + -- member of a node list, and To must be a node list. + + procedure Append_New_To (To : in out List_Id; Node : Node_Or_Entity_Id); + pragma Inline (Append_New_To); + -- Like Append_New, but the arguments are in reverse order + procedure Append_To (To : List_Id; Node : Node_Or_Entity_Id); pragma Inline (Append_To); -- Like Append, but arguments are the other way round diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 92d3003..e0520a9 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -646,17 +646,6 @@ package body Sem_Ch3 is -- present. If errors are found, error messages are posted, and the -- Real_Range_Specification of Def is reset to Empty. - procedure Propagate_Default_Init_Cond_Attributes - (From_Typ : Entity_Id; - To_Typ : Entity_Id; - Parent_To_Derivation : Boolean := False; - Private_To_Full_View : Boolean := False); - -- Subsidiary to routines Build_Derived_Type and Process_Full_View. Inherit - -- all attributes related to pragma Default_Initial_Condition from From_Typ - -- to To_Typ. Flag Parent_To_Derivation should be set when the context is - -- the creation of a derived type. Flag Private_To_Full_View should be set - -- when processing both views of a private type. - procedure Record_Type_Declaration (T : Entity_Id; N : Node_Id; @@ -2567,15 +2556,6 @@ package body Sem_Ch3 is if L = Private_Declarations (Context) then Analyze_Package_Contract (Defining_Entity (Context)); - -- Build the bodies of the default initial condition procedures - -- for all types subject to pragma Default_Initial_Condition. - -- From a purely Ada stand point, this is a freezing activity, - -- however freezing is not available under GNATprove_Mode. To - -- accomodate both scenarios, the bodies are build at the end - -- of private declaration analysis. - - Build_Default_Init_Cond_Procedure_Bodies (L); - -- Otherwise the contract is analyzed at the end of the visible -- declarations. @@ -4639,12 +4619,21 @@ package body Sem_Ch3 is Build_Derived_Record_Type (N, Parent_Type, T); + -- A private extension inherits the Default_Initial_Condition pragma + -- coming from any parent type within the derivation chain. + + if Has_DIC (Parent_Type) then + Set_Has_Inherited_DIC (T); + end if; + -- 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 + if Has_Inherited_Invariants (Parent_Type) + or else Has_Inheritable_Invariants (Parent_Type) + then Set_Has_Inherited_Invariants (T); elsif Present (Interfaces (T)) then @@ -5243,11 +5232,6 @@ package body Sem_Ch3 is 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); @@ -8863,40 +8847,6 @@ package body Sem_Ch3 is end; end if; - -- 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_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 - Iface : Entity_Id; - Iface_Elmt : Elmt_Id; - - begin - 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 (Iface_Elmt); - end loop; - end; - end if; - end if; - -- A type extension is automatically Ghost when one of its -- progenitors is Ghost (SPARK RM 6.9(9)). This property is -- also inherited when the parent type is Ghost, but this is @@ -9128,9 +9078,54 @@ package body Sem_Ch3 is Set_Default_SSO (Derived_Type); end if; - -- Propagate invariant information. The new type has invariants if - -- they are inherited from the parent type, and these invariants can - -- be further inherited, so both flags are set. + -- A derived type inherits the Default_Initial_Condition pragma coming + -- from any parent type within the derivation chain. + + if Has_DIC (Parent_Type) then + Set_Has_Inherited_DIC (Derived_Type); + end if; + + -- 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 not Is_Interface (Derived_Type) then + if Has_Inherited_Invariants (Parent_Type) + or else Has_Inheritable_Invariants (Parent_Type) + then + Set_Has_Inherited_Invariants (Derived_Type); + + elsif Is_Concurrent_Type (Derived_Type) + or else Is_Tagged_Type (Derived_Type) + then + declare + Iface : Entity_Id; + Ifaces : Elist_Id; + Iface_Elmt : Elmt_Id; + + begin + Collect_Interfaces + (T => Derived_Type, + Ifaces_List => Ifaces, + Exclude_Parents => True); + + if Present (Ifaces) then + Iface_Elmt := First_Elmt (Ifaces); + 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 (Iface_Elmt); + end loop; + end if; + end; + end if; + end if; -- We similarly inherit predicates @@ -9142,18 +9137,6 @@ package body Sem_Ch3 is Inherit_Rep_Item_Chain (Derived_Type, Parent_Type); - -- Propagate the attributes related to pragma Default_Initial_Condition - -- from the parent type to the private extension. A derived type always - -- inherits the default initial condition flag from the parent type. If - -- the derived type carries its own Default_Initial_Condition pragma, - -- the flag is later reset in Analyze_Pragma. Note that both flags are - -- mutually exclusive. - - Propagate_Default_Init_Cond_Attributes - (From_Typ => Parent_Type, - To_Typ => Derived_Type, - Parent_To_Derivation => True); - -- If the parent type has delayed rep aspects, then mark the derived -- type as possibly inheriting a delayed rep aspect. @@ -15161,6 +15144,10 @@ package body Sem_Ch3 is -- Actual_Subp is the actual subprogram corresponding with the generic -- subprogram Subp. + ------------------------ + -- Check_Derived_Type -- + ------------------------ + function Check_Derived_Type return Boolean is E : Entity_Id; Elmt : Elmt_Id; @@ -15171,7 +15158,7 @@ package body Sem_Ch3 is begin -- Traverse list of entities in the current scope searching for - -- an incomplete type whose full-view is derived type + -- an incomplete type whose full-view is derived type. E := First_Entity (Scope (Derived_Type)); while Present (E) and then E /= Derived_Type loop @@ -20195,46 +20182,6 @@ package body Sem_Ch3 is Set_Has_Specified_Stream_Output (Full_T); end if; - -- Propagate the attributes related to pragma Default_Initial_Condition - -- from the private to the full view. Note that both flags are mutually - -- exclusive. - - if Has_Default_Init_Cond (Priv_T) - or else Has_Inherited_Default_Init_Cond (Priv_T) - then - Propagate_Default_Init_Cond_Attributes - (From_Typ => Priv_T, - To_Typ => Full_T, - Private_To_Full_View => True); - - -- In the case where the full view is derived from another private type, - -- the attributes related to pragma Default_Initial_Condition must be - -- propagated from the full to the private view to maintain consistency - -- of views. - - -- package Pack is - -- type Parent_Typ is private - -- with Default_Initial_Condition ...; - -- private - -- type Parent_Typ is ...; - -- end Pack; - - -- with Pack; use Pack; - -- package Pack_2 is - -- type Deriv_Typ is private; -- must inherit - -- private - -- type Deriv_Typ is new Parent_Typ; -- must inherit - -- end Pack_2; - - elsif Has_Default_Init_Cond (Full_T) - or else Has_Inherited_Default_Init_Cond (Full_T) - then - Propagate_Default_Init_Cond_Attributes - (From_Typ => Full_T, - To_Typ => Priv_T, - Private_To_Full_View => True); - end if; - if Is_Ghost_Entity (Priv_T) then -- The Ghost policy in effect at the point of declaration and at the @@ -20248,7 +20195,13 @@ package body Sem_Ch3 is Mark_Full_View_As_Ghost (Priv_T, Full_T); end if; - -- Propagate invariant-related attributes from the private view to the + -- Propagate Default_Initial_Condition-related attributes from the + -- partial view to the full view and its base type. + + Propagate_DIC_Attributes (Full_T, From_Typ => Priv_T); + Propagate_DIC_Attributes (Base_Type (Full_T), From_Typ => Priv_T); + + -- Propagate invariant-related attributes from the partial view to the -- full view and its base type. Propagate_Invariant_Attributes (Full_T, From_Typ => Priv_T); @@ -21085,121 +21038,6 @@ package body Sem_Ch3 is end if; end Process_Subtype; - -------------------------------------------- - -- Propagate_Default_Init_Cond_Attributes -- - -------------------------------------------- - - procedure Propagate_Default_Init_Cond_Attributes - (From_Typ : Entity_Id; - To_Typ : Entity_Id; - Parent_To_Derivation : Boolean := False; - Private_To_Full_View : Boolean := False) - is - procedure Remove_Default_Init_Cond_Procedure (Typ : Entity_Id); - -- 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 - Subps : constant Elist_Id := Subprograms_For_Type (Typ); - Subp_Elmt : Elmt_Id; - Subp_Id : Entity_Id; - - begin - 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 - Remove_Elmt (Subps, Subp_Elmt); - exit; - end if; - - Next_Elmt (Subp_Elmt); - end loop; - end if; - end Remove_Default_Init_Cond_Procedure; - - -- Local variables - - Inherit_Procedure : Boolean := False; - - -- Start of processing for Propagate_Default_Init_Cond_Attributes - - begin - if Has_Default_Init_Cond (From_Typ) then - - -- A derived type inherits the attributes from its parent type - - if Parent_To_Derivation then - Set_Has_Inherited_Default_Init_Cond (To_Typ); - - -- A full view shares the attributes with its private view - - else - Set_Has_Default_Init_Cond (To_Typ); - end if; - - Inherit_Procedure := True; - - -- Due to the order of expansion, a derived private type is processed - -- by two routines which both attempt to set the attributes related - -- to pragma Default_Initial_Condition - Build_Derived_Type and then - -- Process_Full_View. - - -- package Pack is - -- type Parent_Typ is private - -- with Default_Initial_Condition ...; - -- private - -- type Parent_Typ is ...; - -- end Pack; - - -- with Pack; use Pack; - -- package Pack_2 is - -- type Deriv_Typ is private - -- with Default_Initial_Condition ...; - -- private - -- type Deriv_Typ is new Parent_Typ; - -- end Pack_2; - - -- When Build_Derived_Type operates, it sets the attributes on the - -- full view without taking into account that the private view may - -- define its own default initial condition procedure. This becomes - -- apparent in Process_Full_View which must undo some of the work by - -- Build_Derived_Type and propagate the attributes from the private - -- to the full view. - - if Private_To_Full_View then - Set_Has_Inherited_Default_Init_Cond (To_Typ, False); - Remove_Default_Init_Cond_Procedure (To_Typ); - end if; - - -- A type must inherit the default initial condition procedure from a - -- parent type when the parent itself is inheriting the procedure or - -- when it is defining one. This circuitry is also used when dealing - -- with the private / full view of a type. - - elsif Has_Inherited_Default_Init_Cond (From_Typ) - or (Parent_To_Derivation - and Present (Get_Pragma - (From_Typ, Pragma_Default_Initial_Condition))) - then - Set_Has_Inherited_Default_Init_Cond (To_Typ); - Inherit_Procedure := True; - end if; - - if Inherit_Procedure - and then No (Default_Init_Cond_Procedure (To_Typ)) - then - Set_Default_Init_Cond_Procedure - (To_Typ, Default_Init_Cond_Procedure (From_Typ)); - end if; - end Propagate_Default_Init_Cond_Attributes; - ----------------------------- -- Record_Type_Declaration -- ----------------------------- diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 55ec81e..9d0eaec 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -39,6 +39,7 @@ with Exp_Ch7; use Exp_Ch7; with Exp_Disp; use Exp_Disp; with Exp_Dist; use Exp_Dist; with Exp_Dbug; use Exp_Dbug; +with Exp_Util; use Exp_Util; with Freeze; use Freeze; with Ghost; use Ghost; with Lib; use Lib; @@ -1453,19 +1454,12 @@ package body Sem_Ch7 is if Is_Type (E) then - -- Each private type subject to pragma Default_Initial_Condition - -- declares a specialized procedure which verifies the assumption - -- of the pragma. The declaration appears in the visible part of - -- the package to allow for being called from the outside. + -- Preanalyze and resolve the Default_Initial_Condition assertion + -- expression at the end of the visible declarations to catch any + -- errors. - if Has_Default_Init_Cond (E) then - Build_Default_Init_Cond_Procedure_Declaration (E); - - -- A private extension inherits the default initial condition - -- procedure from its parent type. - - elsif Has_Inherited_Default_Init_Cond (E) then - Inherit_Default_Init_Cond_Procedure (E); + if Has_DIC (E) then + Build_DIC_Procedure_Body (E); end if; -- Preanalyze and resolve the invariants of a private type at the @@ -1661,18 +1655,28 @@ package body Sem_Ch7 is ("full view of & does not have preelaborable initialization", E); end if; - -- 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 Serious_Errors_Detected > 0 then - if Is_Type (E) - and then not Is_Private_Type (E) - and then Has_Private_Declaration (E) - and then Has_Invariants (E) - and then Serious_Errors_Detected > 0 - then - Build_Invariant_Procedure_Body (E); + -- Preanalyze and resolve the Default_Initial_Condition assertion + -- expression at the end of the private declarations when freezing + -- did not take place due to errors or because the context is a + -- generic unit. + + if Has_DIC (E) then + Build_DIC_Procedure_Body (E); + end if; + + -- 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 not Is_Private_Type (E) + and then Has_Private_Declaration (E) + and then Has_Invariants (E) + then + Build_Invariant_Procedure_Body (E); + end if; end if; Next_Entity (E); @@ -2630,6 +2634,16 @@ package body Sem_Ch7 is Set_Freeze_Node (Priv, Freeze_Node (Full)); + -- Propagate Default_Initial_Condition-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 DIC procedure body. As a result, + -- both the full view and its base type carry the same DIC-related + -- information. + + Propagate_DIC_Attributes (Full, From_Typ => Full_Base); + Propagate_DIC_Attributes (Full_Base, From_Typ => Full); + -- 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 diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 1c01f3e..594bac9 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -2212,6 +2212,11 @@ package body Sem_Ch9 is Set_Must_Have_Preelab_Init (T); end if; + -- Propagate Default_Initial_Condition-related attributes from the + -- private type to the protected type. + + Propagate_DIC_Attributes (T, From_Typ => Def_Id); + -- Propagate invariant-related attributes from the private type to -- the protected type. @@ -3146,6 +3151,11 @@ package body Sem_Ch9 is Set_Must_Have_Preelab_Init (T); end if; + -- Propagate Default_Initial_Condition-related attributes from the + -- private type to the task type. + + Propagate_DIC_Attributes (T, From_Typ => Def_Id); + -- Propagate invariant-related attributes from the private type to -- task type. diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index e623262..967e739 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -1016,7 +1016,7 @@ package body Sem_Elab is return; end if; - Is_DIC_Proc := Is_Nontrivial_Default_Init_Cond_Procedure (Ent); + Is_DIC_Proc := Is_Nontrivial_DIC_Procedure (Ent); -- Elaboration issues in SPARK are reported only for source constructs -- and for nontrivial Default_Initial_Condition procedures. The latter diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 608acd0..b1a193f 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -89,8 +89,6 @@ with Urealp; use Urealp; with Validsw; use Validsw; with Warnsw; use Warnsw; -with GNAT.HTable; use GNAT.HTable; - package body Sem_Prag is ---------------------------------------------- @@ -166,40 +164,6 @@ package body Sem_Prag is Table_Increment => 100, Table_Name => "Name_Externals"); - --------------------------------------------------------- - -- Handling of inherited class-wide pre/postconditions -- - --------------------------------------------------------- - - -- Following AI12-0113, the expression for a class-wide condition is - -- transformed for a subprogram that inherits it, by replacing calls - -- to primitive operations of the original controlling type into the - -- corresponding overriding operations of the derived type. The following - -- hash table manages this mapping, and is expanded on demand whenever - -- such inherited expression needs to be constructed. - - -- The mapping is also used to check whether an inherited operation has - -- a condition that depends on overridden operations. For such an - -- operation we must create a wrapper that is then treated as a normal - -- overriding. In SPARK mode such operations are illegal. - - -- For a given root type there may be several type extensions with their - -- own overriding operations, so at various times a given operation of - -- the root will be mapped into different overridings. The root type is - -- also mapped into the current type extension to indicate that its - -- operations are mapped into the overriding operations of that current - -- type extension. - - subtype Num_Primitives is Integer range 0 .. 510; - function Entity_Hash (E : Entity_Id) return Num_Primitives; - - package Primitives_Mapping is new Gnat.HTable.Simple_Htable - (Header_Num => Num_Primitives, - Key => Entity_Id, - Element => Entity_Id, - No_element => Empty, - Hash => Entity_Hash, - Equal => "="); - ------------------------------------- -- Local Subprograms and Variables -- ------------------------------------- @@ -13784,7 +13748,7 @@ package body Sem_Prag is -- pragma Default_Initial_Condition [ (null | boolean_EXPRESSION) ]; - when Pragma_Default_Initial_Condition => Default_Init_Cond : declare + when Pragma_Default_Initial_Condition => DIC : declare Discard : Boolean; Stmt : Node_Id; Typ : Entity_Id; @@ -13835,13 +13799,21 @@ package body Sem_Prag is -- purposes of legality checks and removal of ignored Ghost code. Mark_Pragma_As_Ghost (N, Typ); - Set_Has_Default_Init_Cond (Typ); - Set_Has_Inherited_Default_Init_Cond (Typ, False); + + -- The pragma signals that the type defines its own DIC assertion + -- expression. + + Set_Has_Own_DIC (Typ); -- Chain the pragma on the rep item chain for further processing Discard := Rep_Item_Too_Late (Typ, N, FOnly => True); - end Default_Init_Cond; + + -- Create the declaration of the procedure which verifies the + -- assertion expression of pragma DIC at runtime. + + Build_DIC_Procedure_Declaration (Typ); + end DIC; ---------------------------------- -- Default_Scalar_Storage_Order -- @@ -16819,18 +16791,6 @@ package body Sem_Prag is Typ : Entity_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); @@ -16924,16 +16884,6 @@ package body Sem_Prag is Set_Has_Inheritable_Invariants (Typ); end if; - 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. @@ -26766,140 +26716,6 @@ package body Sem_Prag is return False; end Appears_In; - --------------------------------- - -- Build_Class_Wide_Expression -- - --------------------------------- - - procedure Build_Class_Wide_Expression - (Prag : Node_Id; - Subp : Entity_Id; - Par_Subp : Entity_Id; - Adjust_Sloc : Boolean) - is - function Replace_Entity (N : Node_Id) return Traverse_Result; - -- Replace reference to formal of inherited operation or to primitive - -- operation of root type, with corresponding entity for derived type, - -- when constructing the class-wide condition of an overriding - -- subprogram. - - -------------------- - -- Replace_Entity -- - -------------------- - - function Replace_Entity (N : Node_Id) return Traverse_Result is - New_E : Entity_Id; - - begin - if Adjust_Sloc then - Adjust_Inherited_Pragma_Sloc (N); - end if; - - if Nkind (N) = N_Identifier - and then Present (Entity (N)) - and then - (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N))) - and then - (Nkind (Parent (N)) /= N_Attribute_Reference - or else Attribute_Name (Parent (N)) /= Name_Class) - then - -- The replacement does not apply to dispatching calls within the - -- condition, but only to calls whose static tag is that of the - -- parent type. - - if Is_Subprogram (Entity (N)) - and then Nkind (Parent (N)) = N_Function_Call - and then Present (Controlling_Argument (Parent (N))) - then - return OK; - end if; - - -- Determine whether entity has a renaming - - New_E := Primitives_Mapping.Get (Entity (N)); - - if Present (New_E) then - Rewrite (N, New_Occurrence_Of (New_E, Sloc (N))); - end if; - - -- Check that there are no calls left to abstract operations if - -- the current subprogram is not abstract. - - if Nkind (Parent (N)) = N_Function_Call - and then N = Name (Parent (N)) - then - if not Is_Abstract_Subprogram (Subp) - and then Is_Abstract_Subprogram (Entity (N)) - then - Error_Msg_Sloc := Sloc (Current_Scope); - Error_Msg_NE - ("cannot call abstract subprogram in inherited condition " - & "for&#", N, Current_Scope); - - -- In SPARK mode, reject an inherited condition for an - -- inherited operation if it contains a call to an overriding - -- operation, because this implies that the pre/postcondition - -- of the inherited operation have changed silently. - - elsif SPARK_Mode = On - and then Warn_On_Suspicious_Contract - and then Present (Alias (Subp)) - and then Present (New_E) - and then Comes_From_Source (New_E) - then - Error_Msg_N - ("cannot modify inherited condition (SPARK RM 6.1.1(1))", - Parent (Subp)); - Error_Msg_Sloc := Sloc (New_E); - Error_Msg_Node_2 := Subp; - Error_Msg_NE - ("\overriding of&# forces overriding of&", - Parent (Subp), New_E); - end if; - end if; - - -- Update type of function call node, which should be the same as - -- the function's return type. - - if Is_Subprogram (Entity (N)) - and then Nkind (Parent (N)) = N_Function_Call - then - Set_Etype (Parent (N), Etype (Entity (N))); - end if; - - -- The whole expression will be reanalyzed - - elsif Nkind (N) in N_Has_Etype then - Set_Analyzed (N, False); - end if; - - return OK; - end Replace_Entity; - - procedure Replace_Condition_Entities is - new Traverse_Proc (Replace_Entity); - - -- Local variables - - Par_Formal : Entity_Id; - Subp_Formal : Entity_Id; - - -- Start of processing for Build_Class_Wide_Expression - - begin - -- Add mapping from old formals to new formals - - Par_Formal := First_Formal (Par_Subp); - Subp_Formal := First_Formal (Subp); - - while Present (Par_Formal) and then Present (Subp_Formal) loop - Primitives_Mapping.Set (Par_Formal, Subp_Formal); - Next_Formal (Par_Formal); - Next_Formal (Subp_Formal); - end loop; - - Replace_Condition_Entities (Prag); - end Build_Class_Wide_Expression; - ----------------------------------- -- Build_Pragma_Check_Equivalent -- ----------------------------------- @@ -27930,15 +27746,6 @@ package body Sem_Prag is end if; end Duplication_Error; - ----------------- - -- Entity_Hash -- - ----------------- - - function Entity_Hash (E : Entity_Id) return Num_Primitives is - begin - return Num_Primitives (E mod 511); - end Entity_Hash; - ------------------------------ -- Find_Encapsulating_State -- ------------------------------ @@ -29780,145 +29587,4 @@ package body Sem_Prag is return Empty; end Test_Case_Arg; - ------------------------------- - -- Update_Primitives_Mapping -- - ------------------------------- - - procedure Update_Primitives_Mapping - (Inher_Id : Entity_Id; - Subp_Id : Entity_Id) - is - function Overridden_Ancestor (S : Entity_Id) return Entity_Id; - -- Locate the primitive operation with the name of S whose controlling - -- type is the dispatching type of Inher_Id. - - ------------------------- - -- Overridden_Ancestor -- - ------------------------- - - function Overridden_Ancestor (S : Entity_Id) return Entity_Id is - Par : constant Entity_Id := Find_Dispatching_Type (Inher_Id); - Anc : Entity_Id; - - begin - Anc := S; - - -- Locate the ancestor subprogram with the proper controlling type - - while Present (Overridden_Operation (Anc)) loop - Anc := Overridden_Operation (Anc); - exit when Find_Dispatching_Type (Anc) = Par; - end loop; - - return Anc; - end Overridden_Ancestor; - - -- Local variables - - Old_Typ : constant Entity_Id := Find_Dispatching_Type (Inher_Id); - Typ : constant Entity_Id := Find_Dispatching_Type (Subp_Id); - Decl : Node_Id; - Old_Elmt : Elmt_Id; - Old_Prim : Entity_Id; - Prim : Entity_Id; - - -- Start of processing for Update_Primitives_Mapping - - begin - -- If the types are already in the map, it has been previously built for - -- some other overriding primitive. - - if Primitives_Mapping.Get (Old_Typ) = Typ then - return; - - else - -- Initialize new mapping with the primitive operations - - Decl := First (List_Containing (Unit_Declaration_Node (Subp_Id))); - - -- Look for primitive operations of the current type that have - -- overridden an operation of the type related to the original - -- class-wide precondition. There may be several intermediate - -- overridings between them. - - while Present (Decl) loop - if Nkind_In (Decl, N_Abstract_Subprogram_Declaration, - N_Subprogram_Declaration) - then - Prim := Defining_Entity (Decl); - - if Is_Subprogram (Prim) - and then Present (Overridden_Operation (Prim)) - and then Find_Dispatching_Type (Prim) = Typ - then - Old_Prim := Overridden_Ancestor (Prim); - - Primitives_Mapping.Set (Old_Prim, Prim); - end if; - end if; - - Next (Decl); - end loop; - - -- Now examine inherited operations. these do not override, but have - -- an alias, which is the entity used in a call. That alias may be - -- inherited or come from source, in which case it may override an - -- earlier operation. We only need to examine inherited functions, - -- that can appear within the inherited expression. - - Prim := First_Entity (Scope (Subp_Id)); - while Present (Prim) loop - if not Comes_From_Source (Prim) - and then Ekind (Prim) = E_Function - and then Present (Alias (Prim)) - then - Old_Prim := Alias (Prim); - - if Comes_From_Source (Old_Prim) then - Old_Prim := Overridden_Ancestor (Old_Prim); - - else - while Present (Alias (Old_Prim)) - and then Scope (Old_Prim) /= Scope (Inher_Id) - loop - Old_Prim := Alias (Old_Prim); - - if Comes_From_Source (Old_Prim) then - Old_Prim := Overridden_Ancestor (Old_Prim); - exit; - end if; - end loop; - end if; - - Primitives_Mapping.Set (Old_Prim, Prim); - end if; - - Next_Entity (Prim); - end loop; - - -- If the parent operation is an interface operation, the overriding - -- indicator is not present. Instead, we get from the interface - -- operation the primitive of the current type that implements it. - - if Is_Interface (Old_Typ) then - Old_Elmt := First_Elmt (Collect_Primitive_Operations (Old_Typ)); - while Present (Old_Elmt) loop - Old_Prim := Node (Old_Elmt); - Prim := Find_Primitive_Covering_Interface (Typ, Old_Prim); - - if Present (Prim) then - Primitives_Mapping.Set (Old_Prim, Prim); - end if; - - Next_Elmt (Old_Elmt); - end loop; - end if; - end if; - - -- Map the types themselves, so that the process is not repeated for - -- other overriding primitives. - - Primitives_Mapping.Set (Old_Typ, Typ); - end Update_Primitives_Mapping; - end Sem_Prag; diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index b229a6c..1155673 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -244,24 +244,6 @@ package Sem_Prag is procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id); -- Perform preanalysis of pragma Test_Case - procedure Build_Class_Wide_Expression - (Prag : Node_Id; - Subp : Entity_Id; - Par_Subp : Entity_Id; - Adjust_Sloc : Boolean); - -- Build the expression for an inherited class-wide condition. Prag is - -- the pragma constructed from the corresponding aspect of the parent - -- subprogram, and Subp is the overriding operation and Par_Subp is - -- the overridden operation that has the condition. Adjust_Sloc is True - -- when the sloc of nodes traversed should be adjusted for the inherited - -- pragma. The routine is also called to check whether an inherited - -- operation that is not overridden but has inherited conditions need - -- a wrapper, because the inherited condition includes calls to other - -- primitives that have been overridden. In that case the first argument - -- is the expression of the original class-wide aspect. In SPARK_Mode, such - -- operation which are just inherited but have modified pre/postconditions - -- are illegal. - function Build_Pragma_Check_Equivalent (Prag : Node_Id; Subp_Id : Entity_Id := Empty; @@ -543,13 +525,4 @@ package Sem_Prag is -- -- Empty if there is no such argument - procedure Update_Primitives_Mapping - (Inher_Id : Entity_Id; - Subp_Id : Entity_Id); - -- Map primitive operations of the parent type to the corresponding - -- operations of the descendant. Note that the descendant type may not be - -- frozen yet, so we cannot use the dispatch table directly. This is called - -- when elaborating a contract for a subprogram, and when freezing a type - -- extension to verify legality rules on inherited conditions. - end Sem_Prag; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 64cbbea..ba64d89 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -37,7 +37,6 @@ with Exp_Disp; use Exp_Disp; with Exp_Util; use Exp_Util; with Fname; use Fname; with Freeze; use Freeze; -with Ghost; use Ghost; with Lib; use Lib; with Lib.Xref; use Lib.Xref; with Namet.Sp; use Namet.Sp; @@ -52,7 +51,6 @@ with Sem_Aux; use Sem_Aux; with Sem_Attr; use Sem_Attr; 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_Prag; use Sem_Prag; @@ -1194,294 +1192,6 @@ package body Sem_Util is return Decl; end Build_Component_Subtype; - ---------------------------------- - -- Build_Default_Init_Cond_Call -- - ---------------------------------- - - function Build_Default_Init_Cond_Call - (Loc : Source_Ptr; - Obj_Id : Entity_Id; - Typ : Entity_Id) return Node_Id - is - Proc_Id : constant Entity_Id := Default_Init_Cond_Procedure (Typ); - Formal_Typ : constant Entity_Id := Etype (First_Formal (Proc_Id)); - - begin - return - Make_Procedure_Call_Statement (Loc, - Name => New_Occurrence_Of (Proc_Id, Loc), - Parameter_Associations => New_List ( - Make_Unchecked_Type_Conversion (Loc, - Subtype_Mark => New_Occurrence_Of (Formal_Typ, Loc), - Expression => New_Occurrence_Of (Obj_Id, Loc)))); - end Build_Default_Init_Cond_Call; - - ---------------------------------------------- - -- Build_Default_Init_Cond_Procedure_Bodies -- - ---------------------------------------------- - - procedure Build_Default_Init_Cond_Procedure_Bodies (Priv_Decls : List_Id) is - procedure Build_Default_Init_Cond_Procedure_Body (Typ : Entity_Id); - -- If type Typ is subject to pragma Default_Initial_Condition, build the - -- body of the procedure which verifies the assumption of the pragma at - -- run time. The generated body is added after the type declaration. - - -------------------------------------------- - -- Build_Default_Init_Cond_Procedure_Body -- - -------------------------------------------- - - procedure Build_Default_Init_Cond_Procedure_Body (Typ : Entity_Id) is - Param_Id : Entity_Id; - -- The entity of the sole formal parameter of the default initial - -- condition procedure. - - procedure Replace_Type_Reference (N : Node_Id); - -- Replace a single reference to type Typ with a reference to formal - -- parameter Param_Id. - - ---------------------------- - -- Replace_Type_Reference -- - ---------------------------- - - procedure Replace_Type_Reference (N : Node_Id) is - begin - Rewrite (N, New_Occurrence_Of (Param_Id, Sloc (N))); - end Replace_Type_Reference; - - procedure Replace_Type_References is - new Replace_Type_References_Generic (Replace_Type_Reference); - - -- Local variables - - Loc : constant Source_Ptr := Sloc (Typ); - Prag : constant Node_Id := - Get_Pragma (Typ, Pragma_Default_Initial_Condition); - Proc_Id : constant Entity_Id := Default_Init_Cond_Procedure (Typ); - Body_Decl : Node_Id; - Expr : Node_Id; - Spec_Decl : Node_Id; - Stmt : Node_Id; - - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - - -- Start of processing for Build_Default_Init_Cond_Procedure_Body - - begin - -- The procedure should be generated only for [sub]types subject to - -- pragma Default_Initial_Condition. Types that inherit the pragma do - -- not get this specialized procedure. - - pragma Assert (Has_Default_Init_Cond (Typ)); - pragma Assert (Present (Prag)); - - -- Nothing to do if the spec was not built. This occurs when the - -- expression of the Default_Initial_Condition is missing or is - -- null. - - if No (Proc_Id) then - return; - - -- Nothing to do if the body was already built - - elsif Present (Corresponding_Body (Unit_Declaration_Node (Proc_Id))) - then - return; - end if; - - -- The related type may be subject to pragma Ghost. Set the mode now - -- to ensure that the analysis and expansion produce Ghost nodes. - - Set_Ghost_Mode_From_Entity (Typ); - - Param_Id := First_Formal (Proc_Id); - - -- The pragma has an argument. Note that the argument is analyzed - -- after all references to the current instance of the type are - -- replaced. - - if Present (Pragma_Argument_Associations (Prag)) then - Expr := - Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))); - - if Nkind (Expr) = N_Null then - Stmt := Make_Null_Statement (Loc); - - -- Preserve the original argument of the pragma by replicating it. - -- Replace all references to the current instance of the type with - -- references to the formal parameter. - - else - Expr := New_Copy_Tree (Expr); - Replace_Type_References (Expr, Typ); - - -- Generate: - -- pragma Check (Default_Initial_Condition, <Expr>); - - Stmt := - Make_Pragma (Loc, - Chars => Name_Check, - Pragma_Argument_Associations => New_List ( - Make_Pragma_Argument_Association (Loc, - Expression => - Make_Identifier (Loc, - Chars => Name_Default_Initial_Condition)), - Make_Pragma_Argument_Association (Loc, - Expression => Expr))); - end if; - - -- Otherwise the pragma appears without an argument - - else - Stmt := Make_Null_Statement (Loc); - end if; - - -- Generate: - -- procedure <Typ>Default_Init_Cond (I : <Typ>) is - -- begin - -- <Stmt>; - -- end <Typ>Default_Init_Cond; - - Spec_Decl := Unit_Declaration_Node (Proc_Id); - Body_Decl := - Make_Subprogram_Body (Loc, - Specification => - Copy_Separate_Tree (Specification (Spec_Decl)), - Declarations => Empty_List, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => New_List (Stmt))); - - -- Link the spec and body of the default initial condition procedure - -- to prevent the generation of a duplicate body. - - Set_Corresponding_Body (Spec_Decl, Defining_Entity (Body_Decl)); - Set_Corresponding_Spec (Body_Decl, Proc_Id); - - Insert_After_And_Analyze (Declaration_Node (Typ), Body_Decl); - Ghost_Mode := Save_Ghost_Mode; - end Build_Default_Init_Cond_Procedure_Body; - - -- Local variables - - Decl : Node_Id; - Typ : Entity_Id; - - -- Start of processing for Build_Default_Init_Cond_Procedure_Bodies - - begin - -- Inspect the private declarations looking for [sub]type declarations - - Decl := First (Priv_Decls); - while Present (Decl) loop - if Nkind_In (Decl, N_Full_Type_Declaration, - N_Subtype_Declaration) - then - Typ := Defining_Entity (Decl); - - -- Guard against partially decorate types due to previous errors - - if Is_Type (Typ) then - - -- If the type is subject to pragma Default_Initial_Condition, - -- generate the body of the internal procedure which verifies - -- the assertion of the pragma at run time. - - if Has_Default_Init_Cond (Typ) then - Build_Default_Init_Cond_Procedure_Body (Typ); - - -- A derived type inherits the default initial condition - -- procedure from its parent type. - - elsif Has_Inherited_Default_Init_Cond (Typ) then - Inherit_Default_Init_Cond_Procedure (Typ); - end if; - end if; - end if; - - Next (Decl); - end loop; - end Build_Default_Init_Cond_Procedure_Bodies; - - --------------------------------------------------- - -- Build_Default_Init_Cond_Procedure_Declaration -- - --------------------------------------------------- - - procedure Build_Default_Init_Cond_Procedure_Declaration (Typ : Entity_Id) is - Loc : constant Source_Ptr := Sloc (Typ); - Prag : constant Node_Id := - Get_Pragma (Typ, Pragma_Default_Initial_Condition); - - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - - Args : List_Id; - Proc_Id : Entity_Id; - - begin - -- The procedure should be generated only for types subject to pragma - -- Default_Initial_Condition. Types that inherit the pragma do not get - -- this specialized procedure. - - pragma Assert (Has_Default_Init_Cond (Typ)); - pragma Assert (Present (Prag)); - - Args := Pragma_Argument_Associations (Prag); - - -- Nothing to do if default initial condition procedure already built - - if Present (Default_Init_Cond_Procedure (Typ)) then - return; - - -- Nothing to do if the default initial condition appears without an - -- expression. - - elsif No (Args) then - return; - - -- Nothing to do if the expression of the default initial condition is - -- null. - - elsif Nkind (Get_Pragma_Arg (First (Args))) = N_Null then - return; - end if; - - -- The related type may be subject to pragma Ghost. Set the mode now to - -- ensure that the analysis and expansion produce Ghost nodes. - - Set_Ghost_Mode_From_Entity (Typ); - - Proc_Id := - Make_Defining_Identifier (Loc, - Chars => New_External_Name (Chars (Typ), "Default_Init_Cond")); - - -- Associate default initial condition procedure with the private type - - Set_Ekind (Proc_Id, E_Procedure); - Set_Is_Default_Init_Cond_Procedure (Proc_Id); - Set_Default_Init_Cond_Procedure (Typ, Proc_Id); - - -- Mark the default initial condition procedure explicitly as Ghost - -- because it does not come from source. - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Proc_Id); - end if; - - -- Generate: - -- procedure <Typ>Default_Init_Cond (Inn : <Typ>); - - Insert_After_And_Analyze (Prag, - Make_Subprogram_Declaration (Loc, - Specification => - Make_Procedure_Specification (Loc, - Defining_Unit_Name => Proc_Id, - Parameter_Specifications => New_List ( - Make_Parameter_Specification (Loc, - Defining_Identifier => Make_Temporary (Loc, 'I'), - Parameter_Type => New_Occurrence_Of (Typ, Loc)))))); - - Ghost_Mode := Save_Ghost_Mode; - end Build_Default_Init_Cond_Procedure_Declaration; - --------------------------- -- Build_Default_Subtype -- --------------------------- @@ -8713,6 +8423,8 @@ package body Sem_Util is Full_Base : out Entity_Id; CRec_Typ : out Entity_Id) is + IP_View : Entity_Id; + begin -- Assume that none of the views can be recovered @@ -8721,24 +8433,10 @@ package body Sem_Util is 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 + if Ekind (Typ) = E_Record_Type and then Is_Concurrent_Record_Type (Typ) then CRec_Typ := Typ; @@ -8746,28 +8444,35 @@ package body Sem_Util is 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 + -- Otherwise the input type denotes an arbitrary type else - Full_Typ := Typ; - Full_Base := Base_Type (Full_Typ); + IP_View := Incomplete_Or_Partial_View (Typ); - if Ekind_In (Full_Typ, E_Protected_Type, E_Task_Type) then - CRec_Typ := Corresponding_Record_Type (Full_Typ); - end if; + -- The input type denotes the full view of a private type - -- The type is the full view of a private type, obtain the partial - -- view. + if Present (IP_View) then + Priv_Typ := IP_View; + Full_Typ := Typ; - if Has_Private_Declaration (Full_Typ) - and then not Is_Private_Type (Full_Typ) - then - Priv_Typ := Incomplete_Or_Partial_View (Full_Typ); + -- The input type is a private type + + elsif Is_Private_Type (Typ) then + Priv_Typ := Typ; + Full_Typ := Full_View (Priv_Typ); + + -- Otherwise the input type does not have any views + + else + Full_Typ := Typ; + end if; - -- The full view of a private type should always have a partial - -- view. + if Present (Full_Typ) then + Full_Base := Base_Type (Full_Typ); - pragma Assert (Present (Priv_Typ)); + if Ekind_In (Full_Typ, E_Protected_Type, E_Task_Type) then + CRec_Typ := Corresponding_Record_Type (Full_Typ); + end if; end if; end if; end Get_Views; @@ -9502,39 +9207,20 @@ package body Sem_Util is ------------------------------------- function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is - Arg : Node_Id; Comp : Entity_Id; Prag : Node_Id; begin - -- A private type and its full view is fully default initialized when it - -- is subject to pragma Default_Initial_Condition without an argument or - -- with a non-null argument. Since any type may act as the full view of - -- a private type, this check must be performed prior to the specialized - -- tests below. + -- A type subject to pragma Default_Initial_Condition is fully default + -- initialized when the pragma appears with a non-null argument. Since + -- any type may act as the full view of a private type, this check must + -- be performed prior to the specialized tests below. - if Has_Default_Init_Cond (Typ) - or else Has_Inherited_Default_Init_Cond (Typ) - then + if Has_DIC (Typ) then Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition); - - -- Pragma Default_Initial_Condition must be present if one of the - -- related entity flags is set. - pragma Assert (Present (Prag)); - Arg := First (Pragma_Argument_Associations (Prag)); - - -- A non-null argument guarantees full default initialization - - if Present (Arg) then - return Nkind (Arg) /= N_Null; - - -- Otherwise the missing argument defaults the pragma to "True" which - -- is considered a non-null argument (see above). - else - return True; - end if; + return Is_Verifiable_DIC_Pragma (Prag); end if; -- A scalar type is fully default initialized if it is subject to aspect @@ -11302,23 +10988,6 @@ package body Sem_Util is return Off * (Expr_Value (Exp) - Expr_Value (Low_Bound ((Ind)))); end Indexed_Component_Bit_Offset; - ----------------------------------------- - -- Inherit_Default_Init_Cond_Procedure -- - ----------------------------------------- - - procedure Inherit_Default_Init_Cond_Procedure (Typ : Entity_Id) is - Par_Typ : constant Entity_Id := Etype (Typ); - - begin - -- A derived type inherits the default initial condition procedure of - -- its parent type. - - if No (Default_Init_Cond_Procedure (Typ)) then - Set_Default_Init_Cond_Procedure - (Typ, Default_Init_Cond_Procedure (Par_Typ)); - end if; - end Inherit_Default_Init_Cond_Procedure; - ---------------------------- -- Inherit_Rep_Item_Chain -- ---------------------------- @@ -13493,20 +13162,16 @@ package body Sem_Util is end if; end Is_Local_Variable_Reference; - ----------------------------------------------- - -- Is_Nontrivial_Default_Init_Cond_Procedure -- - ----------------------------------------------- + --------------------------------- + -- Is_Nontrivial_DIC_Procedure -- + --------------------------------- - function Is_Nontrivial_Default_Init_Cond_Procedure - (Id : Entity_Id) return Boolean - is + function Is_Nontrivial_DIC_Procedure (Id : Entity_Id) return Boolean is Body_Decl : Node_Id; - Stmt : Node_Id; + Stmt : Node_Id; begin - if Ekind (Id) = E_Procedure - and then Is_Default_Init_Cond_Procedure (Id) - then + if Ekind (Id) = E_Procedure and then Is_DIC_Procedure (Id) then Body_Decl := Unit_Declaration_Node (Corresponding_Body (Unit_Declaration_Node (Id))); @@ -13530,7 +13195,7 @@ package body Sem_Util is end if; return False; - end Is_Nontrivial_Default_Init_Cond_Procedure; + end Is_Nontrivial_DIC_Procedure; ------------------------- -- Is_Null_Record_Type -- @@ -15391,6 +15056,21 @@ package body Sem_Util is end if; end Is_Variable; + ------------------------------ + -- Is_Verifiable_DIC_Pragma -- + ------------------------------ + + function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + + begin + -- To qualify as verifiable, a DIC pragma must have a non-null argument + + return + Present (Args) + and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null; + end Is_Verifiable_DIC_Pragma; + --------------------------- -- Is_Visibly_Controlled -- --------------------------- @@ -18481,7 +18161,6 @@ package body Sem_Util is --------------------------- function Primitive_Names_Match (E1, E2 : Entity_Id) return Boolean is - function Non_Internal_Name (E : Entity_Id) return Name_Id; -- Given an internal name, returns the corresponding non-internal name @@ -18701,6 +18380,70 @@ package body Sem_Util is Set_Sloc (Endl, Loc); end Process_End_Label; + -------------------------------- + -- Propagate_Concurrent_Flags -- + -------------------------------- + + procedure Propagate_Concurrent_Flags + (Typ : Entity_Id; + Comp_Typ : Entity_Id) + is + begin + if Has_Task (Comp_Typ) then + Set_Has_Task (Typ); + end if; + + if Has_Protected (Comp_Typ) then + Set_Has_Protected (Typ); + end if; + + if Has_Timing_Event (Comp_Typ) then + Set_Has_Timing_Event (Typ); + end if; + end Propagate_Concurrent_Flags; + + ------------------------------ + -- Propagate_DIC_Attributes -- + ------------------------------ + + procedure Propagate_DIC_Attributes + (Typ : Entity_Id; + From_Typ : Entity_Id) + is + DIC_Proc : 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; + + DIC_Proc := DIC_Procedure (From_Typ); + + -- The setting of the attributes is intentionally conservative. This + -- prevents accidental clobbering of enabled attributes. + + if Has_Inherited_DIC (From_Typ) + and then not Has_Inherited_DIC (Typ) + then + Set_Has_Inherited_DIC (Typ); + end if; + + if Has_Own_DIC (From_Typ) and then not Has_Own_DIC (Typ) then + Set_Has_Own_DIC (Typ); + end if; + + if Present (DIC_Proc) and then No (DIC_Procedure (Typ)) then + Set_DIC_Procedure (Typ, DIC_Proc); + end if; + end if; + end Propagate_DIC_Attributes; + ------------------------------------ -- Propagate_Invariant_Attributes -- ------------------------------------ @@ -18758,28 +18501,6 @@ package body Sem_Util is end if; end Propagate_Invariant_Attributes; - -------------------------------- - -- Propagate_Concurrent_Flags -- - -------------------------------- - - procedure Propagate_Concurrent_Flags - (Typ : Entity_Id; - Comp_Typ : Entity_Id) - is - begin - if Has_Task (Comp_Typ) then - Set_Has_Task (Typ); - end if; - - if Has_Protected (Comp_Typ) then - Set_Has_Protected (Typ); - end if; - - if Has_Timing_Event (Comp_Typ) then - Set_Has_Timing_Event (Typ); - end if; - end Propagate_Concurrent_Flags; - --------------------------------------- -- Record_Possible_Part_Of_Reference -- --------------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 0e95bdd..b79d02c 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -209,24 +209,6 @@ package Sem_Util is -- Determine whether a selected component has a type that depends on -- discriminants, and build actual subtype for it if so. - function Build_Default_Init_Cond_Call - (Loc : Source_Ptr; - Obj_Id : Entity_Id; - Typ : Entity_Id) return Node_Id; - -- Build a call to the default initial condition procedure of type Typ with - -- Obj_Id as the actual parameter. - - procedure Build_Default_Init_Cond_Procedure_Bodies (Priv_Decls : List_Id); - -- Inspect the contents of private declarations Priv_Decls and build the - -- bodies the default initial condition procedures for all types subject - -- to pragma Default_Initial_Condition. - - procedure Build_Default_Init_Cond_Procedure_Declaration (Typ : Entity_Id); - -- If private type Typ is subject to pragma Default_Initial_Condition, - -- build the declaration of the procedure which verifies the assumption - -- of the pragma at runtime. The declaration is inserted after the related - -- pragma. - function Build_Default_Subtype (T : Entity_Id; N : Node_Id) return Entity_Id; @@ -1266,10 +1248,6 @@ package Sem_Util is -- either the value is not yet known before back-end processing or it is -- not known at compile time after back-end processing. - procedure Inherit_Default_Init_Cond_Procedure (Typ : Entity_Id); - -- Inherit the default initial condition procedure from the parent type of - -- derived type Typ. - procedure Inherit_Rep_Item_Chain (Typ : Entity_Id; From_Typ : Entity_Id); -- Inherit the rep item chain of type From_Typ without clobbering any -- existing rep items on Typ's chain. Typ is the destination type. @@ -1528,8 +1506,7 @@ package Sem_Util is -- parameter of the current enclosing subprogram. -- Why are OUT parameters not considered here ??? - function Is_Nontrivial_Default_Init_Cond_Procedure - (Id : Entity_Id) return Boolean; + function Is_Nontrivial_DIC_Procedure (Id : Entity_Id) return Boolean; -- Determine whether entity Id denotes the procedure that verifies the -- assertion expression of pragma Default_Initial_Condition and if it does, -- the encapsulated expression is nontrivial. @@ -1751,6 +1728,10 @@ package Sem_Util is -- default is True since this routine is commonly invoked as part of the -- semantic analysis and it must not be disturbed by the rewriten nodes. + function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean; + -- Determine whether pragma Default_Initial_Condition denoted by Prag has + -- an assertion expression which should be verified at runtime. + function Is_Visibly_Controlled (T : Entity_Id) return Boolean; -- Check whether T is derived from a visibly controlled type. This is true -- if the root type is declared in Ada.Finalization. If T is derived @@ -2050,12 +2031,6 @@ package Sem_Util is -- 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); @@ -2065,6 +2040,18 @@ package Sem_Util is -- by one of these flags. This procedure can only set flags for Typ, and -- never clear them. Comp_Typ is the type of a component or a parent. + procedure Propagate_DIC_Attributes + (Typ : Entity_Id; + From_Typ : Entity_Id); + -- Inherit all Default_Initial_Condition-related attributes from type + -- From_Typ. Typ is the destination type. + + 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 Record_Possible_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id); diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb index f722ada..a3c336b 100644 --- a/gcc/ada/sem_warn.adb +++ b/gcc/ada/sem_warn.adb @@ -1702,20 +1702,21 @@ package body Sem_Warn is ----------------------------- function Is_OK_Fully_Initialized return Boolean is + Prag : Node_Id; + begin if Is_Access_Type (Typ) and then Is_Dereferenced (N) then return False; - -- If a type has Default_Initial_Condition set, or it inherits it, - -- DIC might be specified with a boolean value, meaning that the type - -- is considered to be fully default initialized (SPARK RM 3.1 and - -- SPARK RM 7.3.3). To avoid generating spurious warnings in this - -- case, consider all types with DIC as fully initialized. + -- A type subject to pragma Default_Initial_Condition is fully + -- default initialized when the pragma appears with a non-null + -- argument (SPARK RM 3.1 and SPARK RM 7.3.3). - elsif Has_Default_Init_Cond (Typ) - or else Has_Inherited_Default_Init_Cond (Typ) - then - return True; + elsif Has_DIC (Typ) then + Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition); + pragma Assert (Present (Prag)); + + return Is_Verifiable_DIC_Pragma (Prag); else return Is_Fully_Initialized_Type (Typ); diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index 4059f21..fd486dd 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -1284,6 +1284,14 @@ package body Sinfo is return Node3 (N); end Expression; + function Expression_Copy + (N : Node_Id) return Node_Id is + begin + pragma Assert (False + or else NT (N).Nkind = N_Pragma_Argument_Association); + return Node2 (N); + end Expression_Copy; + function Expressions (N : Node_Id) return List_Id is begin @@ -4555,6 +4563,14 @@ package body Sinfo is Set_Node3_With_Parent (N, Val); end Set_Expression; + procedure Set_Expression_Copy + (N : Node_Id; Val : Node_Id) is + begin + pragma Assert (False + or else NT (N).Nkind = N_Pragma_Argument_Association); + Set_Node2 (N, Val); -- semantic field, no parent set + end Set_Expression_Copy; + procedure Set_Expressions (N : Node_Id; Val : List_Id) is begin diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 1aec086..125f197 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1281,6 +1281,12 @@ package Sinfo is -- target of the assignment or initialization is used to generate the -- left-hand side of individual assignment to each sub-component. + -- Expression_Copy (Node2-Sem) + -- Present in N_Pragma_Argument_Association nodes. Contains a copy of the + -- original expression. This field is best used to store pragma-dependent + -- modifications performed on the original expression such as replacement + -- of the current type instance or substitutions of primitives. + -- First_Inlined_Subprogram (Node3-Sem) -- Present in the N_Compilation_Unit node for the main program. Points -- to a chain of entities for subprograms that are to be inlined. The @@ -2571,6 +2577,7 @@ package Sinfo is -- N_Pragma_Argument_Association -- Sloc points to first token in association -- Chars (Name1) (set to No_Name if no pragma argument identifier) + -- Expression_Copy (Node2-Sem) -- Expression (Node3) ------------------------ @@ -9181,6 +9188,9 @@ package Sinfo is function Expression (N : Node_Id) return Node_Id; -- Node3 + function Expression_Copy + (N : Node_Id) return Node_Id; -- Node2 + function Expressions (N : Node_Id) return List_Id; -- List1 @@ -10227,6 +10237,9 @@ package Sinfo is procedure Set_Expression (N : Node_Id; Val : Node_Id); -- Node3 + procedure Set_Expression_Copy + (N : Node_Id; Val : Node_Id); -- Node2 + procedure Set_Expressions (N : Node_Id; Val : List_Id); -- List1 @@ -11082,7 +11095,7 @@ package Sinfo is N_Pragma_Argument_Association => (1 => True, -- Chars (Name1) - 2 => False, -- unused + 2 => False, -- Expression_Copy (Node2-Sem) 3 => True, -- Expression (Node3) 4 => False, -- unused 5 => False), -- unused @@ -12544,14 +12557,14 @@ package Sinfo is 5 => False), -- unused N_Push_Program_Error_Label => - (1 => False, -- Exception_Label + (1 => False, -- unused 2 => False, -- unused 3 => False, -- unused 4 => False, -- unused 5 => False), -- Exception_Label N_Push_Storage_Error_Label => - (1 => False, -- Exception_Label + (1 => False, -- unused 2 => False, -- unused 3 => False, -- unused 4 => False, -- unused @@ -12790,6 +12803,7 @@ package Sinfo is pragma Inline (Explicit_Actual_Parameter); pragma Inline (Explicit_Generic_Actual_Parameter); pragma Inline (Expression); + pragma Inline (Expression_Copy); pragma Inline (Expressions); pragma Inline (First_Bit); pragma Inline (First_Inlined_Subprogram); @@ -13136,6 +13150,7 @@ package Sinfo is pragma Inline (Set_Explicit_Actual_Parameter); pragma Inline (Set_Explicit_Generic_Actual_Parameter); pragma Inline (Set_Expression); + pragma Inline (Set_Expression_Copy); pragma Inline (Set_Expressions); pragma Inline (Set_First_Bit); pragma Inline (Set_First_Inlined_Subprogram); |