From 96e4fda582406cea5c33cecc54cb4f6d1ba8083f Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Mon, 16 Jul 2018 14:12:33 +0000 Subject: [Ada] Missing error on hidden state in instantiation This patch modifies the analysis of package contracts to split processing which is specific to package instantiations on its own. As a result, the lack of indicator Part_Of can now be properly assessed. ------------ -- Source -- ------------ -- gen_pack.ads generic package Gen_Pack is Pack_Var : Integer := 1; end Gen_Pack; -- gen_wrap.ads with Gen_Pack; generic package Gen_Wrap is Wrap_Var : Integer := 1; package Inst is new Gen_Pack; end Gen_Wrap; -- pack.ads with Gen_Pack; with Gen_Wrap; package Pack with SPARK_Mode => On, Abstract_State => State is procedure Force_Body; private package OK_Inst_1 is new Gen_Pack -- OK with Part_Of => State; -- OK package OK_Inst_2 is new Gen_Pack; -- OK pragma Part_Of (State); -- OK package OK_Inst_3 is new Gen_Wrap -- OK with Part_Of => State; -- OK package OK_Inst_4 is new Gen_Wrap; -- OK pragma Part_Of (State); package Error_Inst_1 is new Gen_Pack; -- Error package Error_Inst_2 is new Gen_Wrap; -- Error end Pack; -- pack.adb package body Pack with SPARK_Mode => On, Refined_State => (State => (OK_Inst_1.Pack_Var, OK_Inst_2.Pack_Var, OK_Inst_3.Wrap_Var, OK_Inst_3.Inst.Pack_Var, OK_Inst_4.Wrap_Var, OK_Inst_4.Inst.Pack_Var)) is procedure Force_Body is null; end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c pack.adb pack.ads:23:12: indicator Part_Of is required in this context (SPARK RM 7.2.6(2)) pack.ads:23:12: "Error_Inst_1" is declared in the private part of package "Pack" pack.ads:24:12: indicator Part_Of is required in this context (SPARK RM 7.2.6(2)) pack.ads:24:12: "Error_Inst_2" is declared in the private part of package "Pack" 2018-07-16 Hristian Kirtchev gcc/ada/ * 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. From-SVN: r262731 --- gcc/ada/contracts.ads | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'gcc/ada/contracts.ads') 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 -- cgit v1.1