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"
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-07-16 Hristian Kirtchev <kirtc...@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.--- gcc/ada/contracts.adb
+++ 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 --
--------------------------------
--- gcc/ada/contracts.ads
+++ 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
--- gcc/ada/sem_prag.adb
+++ 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;
