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, 38 insertions, 0 deletions

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 036cc0cfe48..9a000ae7dc6 100644
--- a/gcc/ada/sem_util.adb
+++ b/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 --
    -------------------------------