[multiple changes]

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.

From-SVN: r230525

gcc/ada/ChangeLog

 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.
 
 2015-11-18  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/einfo.adb

@@ -7301,11 +7301,11 @@ package body Einfo is
         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 @@ package body Einfo is
       end if;
 
       return False;
-   end Has_Non_Null_Refinement;
+   end Has_Non_Null_Visible_Refinement;
 
    -----------------------------
    -- Has_Null_Abstract_State --
@@ -7337,11 +7337,11 @@ package body Einfo is
           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 @@ package body Einfo is
       end if;
 
       return False;
-   end Has_Null_Refinement;
+   end Has_Null_Visible_Refinement;
 
    --------------------
    -- Has_Unmodified --

gcc/ada/einfo.ads

@@ -1761,9 +1761,10 @@ package Einfo is
 --       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 @@ package Einfo is
 --       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 @@ package Einfo is
    --    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 @@ package Einfo is
    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;

gcc/ada/exp_util.adb

@@ -6586,8 +6586,8 @@ package body Exp_Util is
       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 :=

gcc/ada/sem_prag.adb

@@ -23308,7 +23308,7 @@ package body Sem_Prag is
 
                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 @@ package body Sem_Prag is
                   --  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 @@ package body Sem_Prag is
                   --  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 @@ package body Sem_Prag is
                   --  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 @@ package body Sem_Prag is
                --  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 @@ package body Sem_Prag is
                --  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 @@ package body Sem_Prag is
                --  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 @@ package body Sem_Prag is
                --  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 @@ package body Sem_Prag is
             --  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

gcc/ada/sem_util.adb

@@ -9078,6 +9078,25 @@ package body Sem_Util is
       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 @@ package body Sem_Util is
       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 --
    -------------------------------

gcc/ada/sem_util.ads

@@ -1059,9 +1059,19 @@ package Sem_Util is
    --  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