+2015-11-18 Hristian Kirtchev <kirtchev@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.
+
+2015-11-18 Gary Dismukes <dismukes@adacore.com>
+
+ * exp_util.adb: Minor reformatting and typo fixes.
+
2015-11-18 Hristian Kirtchev <kirtchev@adacore.com>
* sem_ch4.adb: Minor reformatting.
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
end if;
return False;
- end Has_Non_Null_Refinement;
+ end Has_Non_Null_Visible_Refinement;
-----------------------------
-- Has_Null_Abstract_State --
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
end if;
return False;
- end Has_Null_Refinement;
+ end Has_Null_Visible_Refinement;
--------------------
-- Has_Unmodified --
-- 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
-- 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
-- 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)
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;
if Is_Private_Type (Unc_Typ)
and then Has_Unknown_Discriminants (Unc_Typ)
then
- -- The caller requests a unque external name for both the private and
- -- the full subtype.
+ -- The caller requests a unique external name for both the private
+ -- and the full subtype.
if Present (Related_Id) then
Full_Subtyp :=
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;
-- 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);
-- 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);
-- 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;
-- 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;
-- 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;
-- 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;
-- 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;
-- 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
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 --
------------------------
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 --
-------------------------------
-- 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
projects / gcc.git / commitdiff