This patch implements two predicates that allow for state revinement queries
while ignoring the region over which a state refinement is visible. No test
possible as this requires an external client of the compiler.
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-11-18 Hristian Kirtchev <kirtc...@adacore.com>
* einfo.adb (Has_Non_Null_Refinement): Rename to
Has_Non_Null_Visible_Refinement.
(Has_Null_Refinement): Rename to Has_Null_Visible_Refinement.
* einfo.ads Update the documentation of
attribute Has_Non_Null_Refinement and attribute Has_Null_Refinement.
(Has_Non_Null_Refinement): Rename to Has_Non_Null_Visible_Refinement
and update occurrences in entities.
(Has_Null_Refinement): Rename to Has_Null_Visible_Refinement and update
occurrences in entities.
* sem_prag.adb (Check_In_Out_States): Update the calls to
Has_[Non_]Null_Refinement.
(Check_Input_States): Update the
calls to Has_[Non_]Null_Refinement.
(Check_Output_States): Update the calls to Has_[Non_]Null_Refinement.
(Check_Proof_In_States): Update the calls to Has_[Non_]Null_Refinement.
(Collect_Global_Item): Update the calls to Has_[Non_]Null_Refinement.
(Is_Null_Refined_State): Update the calls to Has_[Non_]Null_Refinement.
(Match_Item): Update the calls to Has_[Non_]Null_Refinement.
* sem_util.adb (Has_Non_Null_Refinement): New routine.
(Has_Null_Refinement): New routine.
* sem_util.ads (Has_Non_Null_Refinement): New routine.
(Has_Null_Refinement): New routine.
Index: einfo.adb
===================================================================
--- einfo.adb (revision 230522)
+++ einfo.adb (working copy)
@@ -7301,11 +7301,11 @@
and then Present (Non_Limited_View (Id));
end Has_Non_Limited_View;
- -----------------------------
- -- Has_Non_Null_Refinement --
- -----------------------------
+ -------------------------------------
+ -- Has_Non_Null_Visible_Refinement --
+ -------------------------------------
- function Has_Non_Null_Refinement (Id : E) return B is
+ function Has_Non_Null_Visible_Refinement (Id : E) return B is
begin
-- "Refinement" is a concept applicable only to abstract states
@@ -7322,7 +7322,7 @@
end if;
return False;
- end Has_Non_Null_Refinement;
+ end Has_Non_Null_Visible_Refinement;
-----------------------------
-- Has_Null_Abstract_State --
@@ -7337,11 +7337,11 @@
and then Is_Null_State (Node (First_Elmt (Abstract_States (Id))));
end Has_Null_Abstract_State;
- -------------------------
- -- Has_Null_Refinement --
- -------------------------
+ ---------------------------------
+ -- Has_Null_Visible_Refinement --
+ ---------------------------------
- function Has_Null_Refinement (Id : E) return B is
+ function Has_Null_Visible_Refinement (Id : E) return B is
begin
-- "Refinement" is a concept applicable only to abstract states
@@ -7358,7 +7358,7 @@
end if;
return False;
- end Has_Null_Refinement;
+ end Has_Null_Visible_Refinement;
--------------------
-- Has_Unmodified --
Index: einfo.ads
===================================================================
--- einfo.ads (revision 230522)
+++ einfo.ads (working copy)
@@ -1761,9 +1761,10 @@
-- E_Abstract_State entities. True if their Non_Limited_View attribute
-- is present.
--- Has_Non_Null_Refinement (synth)
--- Defined in E_Abstract_State entities. True if the state has at least
--- one variable or state constituent in aspect/pragma Refined_State.
+-- Has_Non_Null_Visible_Refinement (synth)
+-- Defined in E_Abstract_State entities. True if the state has a visible
+-- refinement of at least one variable or state constituent as expressed
+-- in aspect/pragma Refined_State.
-- Has_Non_Standard_Rep (Flag75) [implementation base type only]
-- Defined in all type entities. Set when some representation clause
@@ -1779,9 +1780,9 @@
-- Defined in package entities. True if the package is subject to a null
-- Abstract_State aspect/pragma.
--- Has_Null_Refinement (synth)
--- Defined in E_Abstract_State entities. True if the state has a null
--- refinement in aspect/pragma Refined_State.
+-- Has_Null_Visible_Refinement (synth)
+-- Defined in E_Abstract_State entities. True if the state has a visible
+-- null refinement as expressed in aspect/pragma Refined_State.
-- Has_Object_Size_Clause (Flag172)
-- Defined in entities for types and subtypes. Set if an Object_Size
@@ -5525,8 +5526,8 @@
-- From_Limited_With (Flag159)
-- Has_Visible_Refinement (Flag263)
-- Has_Non_Limited_View (synth)
- -- Has_Non_Null_Refinement (synth)
- -- Has_Null_Refinement (synth)
+ -- Has_Non_Null_Visible_Refinement (synth)
+ -- Has_Null_Visible_Refinement (synth)
-- Is_External_State (synth)
-- Is_Null_State (synth)
-- Is_Synchronized_State (synth)
@@ -7255,9 +7256,9 @@
function Has_Entries (Id : E) return B;
function Has_Foreign_Convention (Id : E) return B;
function Has_Non_Limited_View (Id : E) return B;
- function Has_Non_Null_Refinement (Id : E) return B;
+ function Has_Non_Null_Visible_Refinement (Id : E) return B;
function Has_Null_Abstract_State (Id : E) return B;
- function Has_Null_Refinement (Id : E) return B;
+ function Has_Null_Visible_Refinement (Id : E) return B;
function Implementation_Base_Type (Id : E) return E;
function Is_Base_Type (Id : E) return B;
function Is_Boolean_Type (Id : E) return B;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 230524)
+++ sem_prag.adb (working copy)
@@ -23308,7 +23308,7 @@
return
Ekind (Item_Id) = E_Abstract_State
- and then Has_Null_Refinement (Item_Id);
+ and then Has_Null_Visible_Refinement (Item_Id);
else
return False;
end if;
@@ -23359,7 +23359,7 @@
-- An abstract state with visible null refinement matches
-- null or Empty (special case).
- if Has_Null_Refinement (Dep_Item_Id)
+ if Has_Null_Visible_Refinement (Dep_Item_Id)
and then (No (Ref_Item) or else Nkind (Ref_Item) = N_Null)
then
Record_Item (Dep_Item_Id);
@@ -23368,7 +23368,7 @@
-- An abstract state with visible non-null refinement
-- matches one of its constituents.
- elsif Has_Non_Null_Refinement (Dep_Item_Id) then
+ elsif Has_Non_Null_Visible_Refinement (Dep_Item_Id) then
if Is_Entity_Name (Ref_Item) then
Ref_Item_Id := Entity_Of (Ref_Item);
@@ -23698,7 +23698,7 @@
-- Ensure that all of the constituents are utilized as
-- outputs in pragma Refined_Depends.
- elsif Has_Non_Null_Refinement (Item_Id) then
+ elsif Has_Non_Null_Visible_Refinement (Item_Id) then
Check_Constituent_Usage (Item_Id);
end if;
end if;
@@ -24270,7 +24270,7 @@
-- Ensure that one of the three coverage variants is satisfied
if Ekind (Item_Id) = E_Abstract_State
- and then Has_Non_Null_Refinement (Item_Id)
+ and then Has_Non_Null_Visible_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
@@ -24361,7 +24361,7 @@
-- is of mode Input.
if Ekind (Item_Id) = E_Abstract_State
- and then Has_Non_Null_Refinement (Item_Id)
+ and then Has_Non_Null_Visible_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
@@ -24455,7 +24455,7 @@
-- have mode Output.
if Ekind (Item_Id) = E_Abstract_State
- and then Has_Non_Null_Refinement (Item_Id)
+ and then Has_Non_Null_Visible_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
@@ -24545,7 +24545,7 @@
-- is of mode Proof_In
if Ekind (Item_Id) = E_Abstract_State
- and then Has_Non_Null_Refinement (Item_Id)
+ and then Has_Non_Null_Visible_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
@@ -24750,10 +24750,10 @@
-- be null in which case there are no constituents.
if Ekind (Item_Id) = E_Abstract_State then
- if Has_Null_Refinement (Item_Id) then
+ if Has_Null_Visible_Refinement (Item_Id) then
Has_Null_State := True;
- elsif Has_Non_Null_Refinement (Item_Id) then
+ elsif Has_Non_Null_Visible_Refinement (Item_Id) then
Append_New_Elmt (Item_Id, States);
if Item_Mode = Name_Input then
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 230523)
+++ sem_util.adb (working copy)
@@ -9078,6 +9078,25 @@
end if;
end Has_No_Obvious_Side_Effects;
+ -----------------------------
+ -- Has_Non_Null_Refinement --
+ -----------------------------
+
+ function Has_Non_Null_Refinement (Id : Entity_Id) return Boolean is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+
+ -- For a refinement to be non-null, the first constituent must be
+ -- anything other than null.
+
+ if Present (Refinement_Constituents (Id)) then
+ return
+ Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null;
+ end if;
+
+ return False;
+ end Has_Non_Null_Refinement;
+
------------------------
-- Has_Null_Exclusion --
------------------------
@@ -9168,6 +9187,25 @@
end if;
end Has_Null_Extension;
+ -------------------------
+ -- Has_Null_Refinement --
+ -------------------------
+
+ function Has_Null_Refinement (Id : Entity_Id) return Boolean is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+
+ -- For a refinement to be null, the state's sole constituent must be a
+ -- null.
+
+ if Present (Refinement_Constituents (Id)) then
+ return
+ Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null;
+ end if;
+
+ return False;
+ end Has_Null_Refinement;
+
-------------------------------
-- Has_Overriding_Initialize --
-------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 230522)
+++ sem_util.ads (working copy)
@@ -1059,9 +1059,19 @@
-- routine in Remove_Side_Effects is much more extensive and perhaps could
-- be shared, so that this routine would be more accurate.
+ function Has_Non_Null_Refinement (Id : Entity_Id) return Boolean;
+ -- Determine whether abstract state Id has at least one nonnull constituent
+ -- as expressed in pragma Refined_State. This function does not take into
+ -- account the visible refinement region of abstract state Id.
+
function Has_Null_Exclusion (N : Node_Id) return Boolean;
-- Determine whether node N has a null exclusion
+ function Has_Null_Refinement (Id : Entity_Id) return Boolean;
+ -- Determine whether abstract state Id has a null refinement as expressed
+ -- in pragma Refined_State. This function does not take into account the
+ -- visible refinement region of abstract state Id.
+
function Has_Overriding_Initialize (T : Entity_Id) return Boolean;
-- Predicate to determine whether a controlled type has a user-defined
-- Initialize primitive (and, in Ada 2012, whether that primitive is
