diff options
author | Hristian Kirtchev <kirtchev@adacore.com> | 2018-07-16 14:12:33 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-07-16 14:12:33 +0000 |
commit | 96e4fda582406cea5c33cecc54cb4f6d1ba8083f (patch) | |
tree | 72839e27dd0a55f6f9487796c5262996bec81190 /gcc/ada/contracts.ads | |
parent | 400ad4e950bcd8f0940990ea558b1227d8930285 (diff) | |
download | gcc-96e4fda582406cea5c33cecc54cb4f6d1ba8083f.zip gcc-96e4fda582406cea5c33cecc54cb4f6d1ba8083f.tar.gz gcc-96e4fda582406cea5c33cecc54cb4f6d1ba8083f.tar.bz2 |
[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 <kirtchev@adacore.com>
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
Diffstat (limited to 'gcc/ada/contracts.ads')
-rw-r--r-- | gcc/ada/contracts.ads | 9 |
1 files changed, 8 insertions, 1 deletions
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 |