Pragmas/aspects Refined_Global and Refined_Depends may be applied in
a scope where only partial refinement of abstract states is visible,
as defined in SPARK RM 7.2.4. In such a case, the partial refinement
should be used instead of the full refinement for checking the refined
contracts.
Tested on x86_64-pc-linux-gnu, committed on trunk
2016-10-12 Yannick Moy <m...@adacore.com>
* einfo.adb, einfo.ads (Has_Partial_Visible_Refinement): New flag
in abtract states.
(Has_Non_Null_Visible_Refinement): Return true for patial refinement.
(Partial_Refinement_Constituents): New function returns the full or
partial refinement constituents depending on scope.
* sem_ch3.adb (Analyze_Declarations): Remove partial visible
refinements when exiting the scope of a package spec or body
and those partial refinements are not in scope afterwards.
* sem_ch7.adb, sem_ch7.ads (Install_Partial_Declarations): Mark
abstract states of parent units with partial refinement so that
it is visible.
* sem_prag.adb (Analyze_Part_Of_In_Decl_Part): Mark enclosing
abstract state if any as having partial refinement in that scope.
(Analyze_Refined_Global_In_Decl_Part): Check constituent usage
based on full or partial refinement depending on scope.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 241041)
+++ sem_ch3.adb (working copy)
@@ -2178,10 +2178,17 @@
-- case, add a proper spec if the body lacks one. The spec is inserted
-- before Body_Decl and immediately analyzed.
+ procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id);
+ -- Spec_Id is the entity of a package that may define abstract states,
+ -- and in the case of a child unit, whose ancestors may define abstract
+ -- states. If the states have partial visible refinement, remove the
+ -- partial visibility of each constituent at the end of the package
+ -- spec and body declarations.
+
procedure Remove_Visible_Refinements (Spec_Id : Entity_Id);
-- Spec_Id is the entity of a package that may define abstract states.
-- If the states have visible refinement, remove the visibility of each
- -- constituent at the end of the package body declarations.
+ -- constituent at the end of the package body declaration.
-----------------
-- Adjust_Decl --
@@ -2335,6 +2342,29 @@
Insert_Before_And_Analyze (Body_Decl, Decl);
end Handle_Late_Controlled_Primitive;
+ ----------------------------------------
+ -- Remove_Partial_Visible_Refinements --
+ ----------------------------------------
+
+ procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id) is
+ State_Elmt : Elmt_Id;
+ begin
+ if Present (Abstract_States (Spec_Id)) then
+ State_Elmt := First_Elmt (Abstract_States (Spec_Id));
+ while Present (State_Elmt) loop
+ Set_Has_Partial_Visible_Refinement (Node (State_Elmt), False);
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+
+ -- For a child unit, also hide the partial state refinement from
+ -- ancestor packages.
+
+ if Is_Child_Unit (Spec_Id) then
+ Remove_Partial_Visible_Refinements (Scope (Spec_Id));
+ end if;
+ end Remove_Partial_Visible_Refinements;
+
--------------------------------
-- Remove_Visible_Refinements --
--------------------------------
@@ -2576,6 +2606,15 @@
-- restore the original state conditions.
Remove_Visible_Refinements (Corresponding_Spec (Context));
+ Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
+
+ elsif Nkind (Context) = N_Package_Declaration then
+
+ -- Partial state refinements are visible up to the end of the
+ -- package spec declarations. Hide the partial state refinements
+ -- from visibility to restore the original state conditions.
+
+ Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
end if;
-- Verify that all abstract states found in any package declared in
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 241024)
+++ sem_ch7.adb (working copy)
@@ -2275,6 +2275,34 @@
Next_Entity (Id);
end loop;
+ -- An abstract state is partially refined when it has at least one
+ -- Part_Of constituent. Since these constituents are being installed
+ -- into visibility, update the partial refinement status of any state
+ -- defined in the associated package, subject to at least one Part_Of
+ -- constituent.
+
+ if Ekind_In (P, E_Generic_Package, E_Package) then
+ declare
+ States : constant Elist_Id := Abstract_States (P);
+ State_Elmt : Elmt_Id;
+ State_Id : Entity_Id;
+
+ begin
+ if Present (States) then
+ State_Elmt := First_Elmt (States);
+ while Present (State_Elmt) loop
+ State_Id := Node (State_Elmt);
+
+ if Present (Part_Of_Constituents (State_Id)) then
+ Set_Has_Partial_Visible_Refinement (State_Id);
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end;
+ end if;
+
-- Indicate that the private part is currently visible, so it can be
-- properly reset on exit.
Index: sem_ch7.ads
===================================================================
--- sem_ch7.ads (revision 241024)
+++ sem_ch7.ads (working copy)
@@ -46,10 +46,10 @@
-- On entrance to a package body, make declarations in package spec
-- immediately visible.
--
- -- When compiling the body of a package, both routines are called in
+ -- When compiling the body of a package, both routines are called in
-- succession. When compiling the body of a child package, the call
-- to Install_Private_Declaration is immediate for private children,
- -- but is deferred until the compilation of the private part of the
+ -- but is deferred until the compilation of the private part of the
-- child for public child packages.
function Unit_Requires_Body
Index: einfo.adb
===================================================================
--- einfo.adb (revision 241024)
+++ einfo.adb (working copy)
@@ -610,8 +610,8 @@
-- Is_Actual_Subtype Flag293
-- Has_Pragma_Unused Flag294
-- Is_Ignored_Transient Flag295
+ -- Has_Partial_Visible_Refinement Flag296
- -- (unused) Flag296
-- (unused) Flag297
-- (unused) Flag298
-- (unused) Flag299
@@ -1682,6 +1682,12 @@
return Flag232 (Id);
end Has_Own_Invariants;
+ function Has_Partial_Visible_Refinement (Id : E) return B is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ return Flag296 (Id);
+ end Has_Partial_Visible_Refinement;
+
function Has_Per_Object_Constraint (Id : E) return B is
begin
return Flag154 (Id);
@@ -4698,6 +4704,12 @@
Set_Flag232 (Id, V);
end Set_Has_Own_Invariants;
+ procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True) is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Set_Flag296 (Id, V);
+ end Set_Has_Partial_Visible_Refinement;
+
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True) is
begin
Set_Flag154 (Id, V);
@@ -7485,13 +7497,14 @@
pragma Assert (Ekind (Id) = E_Abstract_State);
Constits := Refinement_Constituents (Id);
- -- For a refinement to be non-null, the first constituent must be
- -- anything other than null.
+ -- A partial refinement is always non-null. For a full refinement to be
+ -- non-null, the first constituent must be anything other than null.
return
- Has_Visible_Refinement (Id)
- and then Present (Constits)
- and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
+ Has_Partial_Visible_Refinement (Id)
+ or else (Has_Visible_Refinement (Id)
+ and then Present (Constits)
+ and then Nkind (Node (First_Elmt (Constits))) /= N_Null);
end Has_Non_Null_Visible_Refinement;
-----------------------------
@@ -8370,6 +8383,29 @@
return Empty;
end Partial_Invariant_Procedure;
+ -------------------------------------
+ -- Partial_Refinement_Constituents --
+ -------------------------------------
+
+ function Partial_Refinement_Constituents (Id : E) return L is
+ Constits : Elist_Id;
+
+ begin
+ -- "Refinement" is a concept applicable only to abstract states
+
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Constits := Refinement_Constituents (Id);
+
+ -- A refinement may be partially visible when objects declared in the
+ -- private part of a package are subject to a Part_Of indicator.
+
+ if No (Constits) then
+ Constits := Part_Of_Constituents (Id);
+ end if;
+
+ return Constits;
+ end Partial_Refinement_Constituents;
+
------------------------
-- Predicate_Function --
------------------------
Index: einfo.ads
===================================================================
--- einfo.ads (revision 241024)
+++ einfo.ads (working copy)
@@ -1812,6 +1812,14 @@
-- one invariant of its own. The flag is also set on the full view of a
-- private extension or a private type for completeness.
+-- Has_Partial_Visible_Refinement (Flag296)
+-- Defined in E_Abstract_State entities. Set when a state has at least
+-- one refinement constituent subject to indicator Part_Of, and analysis
+-- is in the region between the declaration of the first constituent for
+-- this abstract state (in the private part of the package) and the end
+-- of the package spec or body with visibility over this private part
+-- (which includes the package itself and its child packages).
+
-- Has_Per_Object_Constraint (Flag154)
-- Defined in E_Component entities. Set if the subtype of the component
-- has a per object constraint. Per object constraints result from the
@@ -3780,6 +3788,11 @@
-- 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.
+-- Partial_Refinement_Constituents (synthesized)
+-- Present in abstract state entities. Contains the constituents that
+-- refine the state in its private part, in other words, all the hidden
+-- states that indicate this abstract state in a Part_Of aspect/pragma.
+
-- Partial_View_Has_Unknown_Discr (Flag280)
-- Present in all types. Set to Indicate that the partial view of a type
-- has unknown discriminants. A default initialization of an object of
@@ -5619,6 +5632,7 @@
-- Non_Limited_View (Node19)
-- Encapsulating_State (Node32)
-- From_Limited_With (Flag159)
+ -- Has_Partial_Visible_Refinement (Flag296)
-- Has_Visible_Refinement (Flag263)
-- Has_Non_Limited_View (synth)
-- Has_Non_Null_Visible_Refinement (synth)
@@ -5626,6 +5640,7 @@
-- Is_External_State (synth)
-- Is_Null_State (synth)
-- Is_Synchronized_State (synth)
+ -- Partial_Refinement_Constituents (synth)
-- E_Access_Protected_Subprogram_Type
-- Equivalent_Type (Node18)
@@ -6977,6 +6992,7 @@
function Has_Object_Size_Clause (Id : E) return B;
function Has_Out_Or_In_Out_Parameter (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;
function Has_Pragma_Controlled (Id : E) return B;
function Has_Pragma_Elaborate_Body (Id : E) return B;
@@ -7412,6 +7428,7 @@
function Number_Entries (Id : E) return Nat;
function Number_Formals (Id : E) return Pos;
function Parameter_Mode (Id : E) return Formal_Kind;
+ function Partial_Refinement_Constituents (Id : E) return L;
function Primitive_Operations (Id : E) return L;
function Root_Type (Id : E) return E;
function Safe_Emax_Value (Id : E) return U;
@@ -7652,6 +7669,7 @@
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_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);
procedure Set_Has_Pragma_Controlled (Id : E; V : B := True);
procedure Set_Has_Pragma_Elaborate_Body (Id : E; V : B := True);
@@ -8444,6 +8462,7 @@
pragma Inline (Has_Object_Size_Clause);
pragma Inline (Has_Out_Or_In_Out_Parameter);
pragma Inline (Has_Own_Invariants);
+ pragma Inline (Has_Partial_Visible_Refinement);
pragma Inline (Has_Per_Object_Constraint);
pragma Inline (Has_Pragma_Controlled);
pragma Inline (Has_Pragma_Elaborate_Body);
@@ -8959,6 +8978,7 @@
pragma Inline (Set_Has_Object_Size_Clause);
pragma Inline (Set_Has_Out_Or_In_Out_Parameter);
pragma Inline (Set_Has_Own_Invariants);
+ pragma Inline (Set_Has_Partial_Visible_Refinement);
pragma Inline (Set_Has_Per_Object_Constraint);
pragma Inline (Set_Has_Pragma_Controlled);
pragma Inline (Set_Has_Pragma_Elaborate_Body);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 241041)
+++ sem_prag.adb (working copy)
@@ -3410,6 +3410,13 @@
Append_Elmt (Var_Id, Constits);
Set_Encapsulating_State (Var_Id, Encap_Id);
+
+ -- A Part_Of constituent partially refines an abstract state. This
+ -- property does not apply to protected or task units.
+
+ if Ekind (Encap_Id) = E_Abstract_State then
+ Set_Has_Partial_Visible_Refinement (Encap_Id);
+ end if;
end if;
-- Emit a clarification message when the encapsulator is undefined,
@@ -18717,7 +18724,7 @@
Add_Contract_Item (N, Item_Id);
- -- A variable may act as consituent of a single concurrent type
+ -- A variable may act as constituent of a single concurrent type
-- which in turn could be declared after the variable. Due to this
-- discrepancy, the full analysis of indicator Part_Of is delayed
-- until the end of the enclosing declarative region (see routine
@@ -24051,7 +24058,7 @@
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Posted : Boolean := False;
@@ -24614,7 +24621,7 @@
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Has_Missing : Boolean := False;
@@ -24753,7 +24760,7 @@
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
In_Seen : Boolean := False;
@@ -24853,7 +24860,7 @@
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Posted : Boolean := False;
@@ -24952,7 +24959,7 @@
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Proof_In_Seen : Boolean := False;
@@ -25083,7 +25090,10 @@
if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
and then Present (Encapsulating_State (Item_Id))
- and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
+ and then
+ (Has_Visible_Refinement (Encapsulating_State (Item_Id))
+ or else
+ Has_Partial_Visible_Refinement (Encapsulating_State (Item_Id)))
and then Contains (States, Encapsulating_State (Item_Id))
then
if Global_Mode = Name_Input then
@@ -25438,10 +25448,10 @@
-- Non-instance case
else
- -- The corresponding Global pragma must mention at least one state
- -- witha visible refinement at the point Refined_Global is processed.
- -- States with null refinements need Refined_Global pragma
- -- (SPARK RM 7.2.4(2)).
+ -- The corresponding Global pragma must mention at least one
+ -- state with a visible refinement at the point Refined_Global
+ -- is processed. States with null refinements need Refined_Global
+ -- pragma (SPARK RM 7.2.4(2)).
if not Has_In_State
and then not Has_In_Out_State
