diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 13 | ||||
| -rw-r--r-- | gcc/ada/contracts.adb | 79 | ||||
| -rw-r--r-- | gcc/ada/contracts.ads | 9 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 6 |
4 files changed, 92 insertions, 15 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6909066..a72e80f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,18 @@ 2018-07-16 Hristian Kirtchev <kirtchev@adacore.com> + * contracts.adb (Analyze_Contracts): Add specialized processing for + package instantiation contracts. + (Analyze_Package_Contract): Remove the verification of a missing + Part_Of indicator. + (Analyze_Package_Instantiation_Contract): New routine. + * contracts.ads (Analyze_Package_Contract): Update the comment on + usage. + * sem_prag.adb (Check_Missing_Part_Of): Ensure that the entity of the + instance is being examined when trying to determine whether a package + instantiation needs a Part_Of indicator. + +2018-07-16 Hristian Kirtchev <kirtchev@adacore.com> + * einfo.adb, exp_ch7.adb, exp_ch9.adb, exp_unst.adb, inline.adb, sem.adb, sem_ch12.adb, sem_ch13.adb, sem_ch3.adb, sem_eval.adb, sem_util.adb: Minor reformatting. diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 104fd16..69cece9 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -53,6 +53,13 @@ with Tbuild; use Tbuild; package body Contracts is + procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id); + -- Analyze all delayed pragmas chained on the contract of package + -- instantiation Inst_Id as if they appear at the end of a declarative + -- region. The pragmas in question are: + -- + -- Part_Of + procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id); -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the -- contract-only subprogram body of eligible subprograms found in L, adds @@ -386,6 +393,11 @@ package body Contracts is elsif Nkind (Decl) = N_Object_Declaration then Analyze_Object_Contract (Defining_Entity (Decl)); + -- Package instantiation + + elsif Nkind (Decl) = N_Package_Instantiation then + Analyze_Package_Instantiation_Contract (Defining_Entity (Decl)); + -- Protected units elsif Nkind_In (Decl, N_Protected_Type_Declaration, @@ -1074,17 +1086,6 @@ package body Contracts is end if; end if; - -- Check whether the lack of indicator Part_Of agrees with the placement - -- of the package instantiation with respect to the state space. - - if Is_Generic_Instance (Pack_Id) then - Prag := Get_Pragma (Pack_Id, Pragma_Part_Of); - - if No (Prag) then - Check_Missing_Part_Of (Pack_Id); - end if; - end if; - -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. @@ -1100,6 +1101,62 @@ package body Contracts is end if; end Analyze_Package_Contract; + -------------------------------------------- + -- Analyze_Package_Instantiation_Contract -- + -------------------------------------------- + + -- WARNING: This routine manages SPARK regions. Return statements must be + -- replaced by gotos which jump to the end of the routine and restore the + -- SPARK mode. + + procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id) is + Inst_Spec : constant Node_Id := + Instance_Spec (Unit_Declaration_Node (Inst_Id)); + + Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; + Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; + -- Save the SPARK_Mode-related data to restore on exit + + Pack_Id : Entity_Id; + Prag : Node_Id; + + begin + -- Nothing to do when the package instantiation is erroneous or left + -- partially decorated. + + if No (Inst_Spec) then + return; + end if; + + Pack_Id := Defining_Entity (Inst_Spec); + Prag := Get_Pragma (Pack_Id, Pragma_Part_Of); + + -- Due to the timing of contract analysis, delayed pragmas may be + -- subject to the wrong SPARK_Mode, usually that of the enclosing + -- context. To remedy this, restore the original SPARK_Mode of the + -- related package. + + Set_SPARK_Mode (Pack_Id); + + -- Check whether the lack of indicator Part_Of agrees with the placement + -- of the package instantiation with respect to the state space. Nested + -- package instantiations do not need to be checked because they inherit + -- Part_Of indicator of the outermost package instantiation (see routine + -- Propagate_Part_Of in Sem_Prag). + + if In_Instance then + null; + + elsif No (Prag) then + Check_Missing_Part_Of (Pack_Id); + end if; + + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. + + Restore_SPARK_Mode (Saved_SM, Saved_SMP); + end Analyze_Package_Instantiation_Contract; + -------------------------------- -- Analyze_Protected_Contract -- -------------------------------- diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index 4a0997f..46f52d1 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -35,6 +35,7 @@ package Contracts is -- [generic] package, package body, protected unit, [generic] subprogram, -- subprogram body, variable or task unit denoted by Id. The following are -- valid pragmas: + -- -- Abstract_State -- Async_Readers -- Async_Writers @@ -66,6 +67,7 @@ package Contracts is -- Analyze all delayed pragmas chained on the contract of entry or -- subprogram body Body_Id as if they appeared at the end of a declarative -- region. Pragmas in question are: + -- -- Contract_Cases (stand alone subprogram body) -- Depends (stand alone subprogram body) -- Global (stand alone subprogram body) @@ -82,6 +84,7 @@ package Contracts is -- Analyze all delayed pragmas chained on the contract of entry or -- subprogram Subp_Id as if they appeared at the end of a declarative -- region. The pragmas in question are: + -- -- Contract_Cases -- Depends -- Global @@ -98,6 +101,7 @@ package Contracts is -- Analyze all delayed pragmas chained on the contract of object Obj_Id as -- if they appeared at the end of the declarative region. The pragmas to be -- considered are: + -- -- Async_Readers -- Async_Writers -- Depends (single concurrent object) @@ -115,6 +119,7 @@ package Contracts is -- Analyze all delayed pragmas chained on the contract of package body -- Body_Id as if they appeared at the end of a declarative region. The -- pragmas that are considered are: + -- -- Refined_State -- -- Freeze_Id is the entity of a [generic] package body or a [generic] @@ -124,9 +129,9 @@ package Contracts is -- Analyze all delayed pragmas chained on the contract of package Pack_Id -- as if they appeared at the end of a declarative region. The pragmas -- that are considered are: + -- -- Initial_Condition -- Initializes - -- Part_Of procedure Analyze_Protected_Contract (Prot_Id : Entity_Id); -- Analyze all delayed pragmas chained on the contract of protected unit @@ -137,6 +142,7 @@ package Contracts is -- Analyze all delayed pragmas chained on the contract of subprogram body -- stub Stub_Id as if they appeared at the end of a declarative region. The -- pragmas in question are: + -- -- Contract_Cases -- Depends -- Global @@ -151,6 +157,7 @@ package Contracts is -- Analyze all delayed pragmas chained on the contract of task unit Task_Id -- as if they appeared at the end of a declarative region. The pragmas in -- question are: + -- -- Depends -- Global diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index a88b37d..6bd5462 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -28897,9 +28897,9 @@ package body Sem_Prag is -- A package instantiation does not need a Part_Of indicator when the -- related generic template has no visible state. - elsif Ekind (Pack_Id) = E_Package - and then Is_Generic_Instance (Pack_Id) - and then not Has_Visible_State (Pack_Id) + elsif Ekind (Item_Id) = E_Package + and then Is_Generic_Instance (Item_Id) + and then not Has_Visible_State (Item_Id) then null; |