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.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@230525 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 10 insertions, 10 deletions

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index be42aaa390c..d113a2c2654 100644
--- a/gcc/ada/sem_prag.adb
+++ b/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