[multiple changes]

2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Is_Matching_Input): Account
	for the case where a state with a null refinement appears as
	the last input of a refinement clause.

2013-10-17  Robert Dewar  <dewar@adacore.com>

	* sem_aux.ads, sem_aux.adb: Minor reformatting.

From-SVN: r203766

4 files changed, 128 insertions, 104 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ecda517..39b8d24 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,15 @@
 2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* sem_prag.adb (Is_Matching_Input): Account
+	for the case where a state with a null refinement appears as
+	the last input of a refinement clause.
+
+2013-10-17  Robert Dewar  <dewar@adacore.com>
+
+	* sem_aux.ads, sem_aux.adb: Minor reformatting.
+
+2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* aspects.adb, aspects.ads, sem_prag.ads: Remove all entries
 	for Refined_Pre from the various tables.
 	* par-prag.adb: Remove the entry for Refined_Pre from the list
diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb
index 24470ed..d67517e 100644
--- a/gcc/ada/sem_aux.adb
+++ b/gcc/ada/sem_aux.adb
@@ -813,105 +813,6 @@ package body Sem_Aux is
       end if;
    end Is_Generic_Formal;
 
-   ---------------------
-   -- Is_Limited_View --
-   ---------------------
-
-   function Is_Limited_View (Ent : Entity_Id) return Boolean is
-      Btype : constant Entity_Id := Available_View (Base_Type (Ent));
-
-   begin
-      if Is_Limited_Record (Btype) then
-         return True;
-
-      elsif Ekind (Btype) = E_Limited_Private_Type
-        and then Nkind (Parent (Btype)) = N_Formal_Type_Declaration
-      then
-         return not In_Package_Body (Scope ((Btype)));
-
-      elsif Is_Private_Type (Btype) then
-
-         --  AI05-0063: A type derived from a limited private formal type is
-         --  not immutably limited in a generic body.
-
-         if Is_Derived_Type (Btype)
-           and then Is_Generic_Type (Etype (Btype))
-         then
-            if not Is_Limited_Type (Etype (Btype)) then
-               return False;
-
-            --  A descendant of a limited formal type is not immutably limited
-            --  in the generic body, or in the body of a generic child.
-
-            elsif Ekind (Scope (Etype (Btype))) = E_Generic_Package then
-               return not In_Package_Body (Scope (Btype));
-
-            else
-               return False;
-            end if;
-
-         else
-            declare
-               Utyp : constant Entity_Id := Underlying_Type (Btype);
-            begin
-               if No (Utyp) then
-                  return False;
-               else
-                  return Is_Limited_View (Utyp);
-               end if;
-            end;
-         end if;
-
-      elsif Is_Concurrent_Type (Btype) then
-         return True;
-
-      elsif Is_Record_Type (Btype) then
-
-         --  Note that we return True for all limited interfaces, even though
-         --  (unsynchronized) limited interfaces can have descendants that are
-         --  nonlimited, because this is a predicate on the type itself, and
-         --  things like functions with limited interface results need to be
-         --  handled as build in place even though they might return objects
-         --  of a type that is not inherently limited.
-
-         if Is_Class_Wide_Type (Btype) then
-            return Is_Limited_View (Root_Type (Btype));
-
-         else
-            declare
-               C : Entity_Id;
-
-            begin
-               C := First_Component (Btype);
-               while Present (C) loop
-
-                  --  Don't consider components with interface types (which can
-                  --  only occur in the case of a _parent component anyway).
-                  --  They don't have any components, plus it would cause this
-                  --  function to return true for nonlimited types derived from
-                  --  limited interfaces.
-
-                  if not Is_Interface (Etype (C))
-                    and then Is_Limited_View (Etype (C))
-                  then
-                     return True;
-                  end if;
-
-                  C := Next_Component (C);
-               end loop;
-            end;
-
-            return False;
-         end if;
-
-      elsif Is_Array_Type (Btype) then
-         return Is_Limited_View (Component_Type (Btype));
-
-      else
-         return False;
-      end if;
-   end Is_Limited_View;
-
    -------------------------------
    -- Is_Immutably_Limited_Type --
    -------------------------------
@@ -1081,6 +982,105 @@ package body Sem_Aux is
       end if;
    end Is_Limited_Type;
 
+   ---------------------
+   -- Is_Limited_View --
+   ---------------------
+
+   function Is_Limited_View (Ent : Entity_Id) return Boolean is
+      Btype : constant Entity_Id := Available_View (Base_Type (Ent));
+
+   begin
+      if Is_Limited_Record (Btype) then
+         return True;
+
+      elsif Ekind (Btype) = E_Limited_Private_Type
+        and then Nkind (Parent (Btype)) = N_Formal_Type_Declaration
+      then
+         return not In_Package_Body (Scope ((Btype)));
+
+      elsif Is_Private_Type (Btype) then
+
+         --  AI05-0063: A type derived from a limited private formal type is
+         --  not immutably limited in a generic body.
+
+         if Is_Derived_Type (Btype)
+           and then Is_Generic_Type (Etype (Btype))
+         then
+            if not Is_Limited_Type (Etype (Btype)) then
+               return False;
+
+            --  A descendant of a limited formal type is not immutably limited
+            --  in the generic body, or in the body of a generic child.
+
+            elsif Ekind (Scope (Etype (Btype))) = E_Generic_Package then
+               return not In_Package_Body (Scope (Btype));
+
+            else
+               return False;
+            end if;
+
+         else
+            declare
+               Utyp : constant Entity_Id := Underlying_Type (Btype);
+            begin
+               if No (Utyp) then
+                  return False;
+               else
+                  return Is_Limited_View (Utyp);
+               end if;
+            end;
+         end if;
+
+      elsif Is_Concurrent_Type (Btype) then
+         return True;
+
+      elsif Is_Record_Type (Btype) then
+
+         --  Note that we return True for all limited interfaces, even though
+         --  (unsynchronized) limited interfaces can have descendants that are
+         --  nonlimited, because this is a predicate on the type itself, and
+         --  things like functions with limited interface results need to be
+         --  handled as build in place even though they might return objects
+         --  of a type that is not inherently limited.
+
+         if Is_Class_Wide_Type (Btype) then
+            return Is_Limited_View (Root_Type (Btype));
+
+         else
+            declare
+               C : Entity_Id;
+
+            begin
+               C := First_Component (Btype);
+               while Present (C) loop
+
+                  --  Don't consider components with interface types (which can
+                  --  only occur in the case of a _parent component anyway).
+                  --  They don't have any components, plus it would cause this
+                  --  function to return true for nonlimited types derived from
+                  --  limited interfaces.
+
+                  if not Is_Interface (Etype (C))
+                    and then Is_Limited_View (Etype (C))
+                  then
+                     return True;
+                  end if;
+
+                  C := Next_Component (C);
+               end loop;
+            end;
+
+            return False;
+         end if;
+
+      elsif Is_Array_Type (Btype) then
+         return Is_Limited_View (Component_Type (Btype));
+
+      else
+         return False;
+      end if;
+   end Is_Limited_View;
+
    ----------------------
    -- Nearest_Ancestor --
    ----------------------
diff --git a/gcc/ada/sem_aux.ads b/gcc/ada/sem_aux.ads
index 0e2818e..49d75ac 100644
--- a/gcc/ada/sem_aux.ads
+++ b/gcc/ada/sem_aux.ads
@@ -283,7 +283,7 @@ package Sem_Aux is
    function Is_Immutably_Limited_Type (Ent : Entity_Id) return Boolean;
    --  Implements definition in Ada 2012 RM-7.5 (8.1/3). This differs from the
    --  following predicate in that an untagged record with immutably limited
-   --  components is NOT by itself immutably limited. This matters, eg. when
+   --  components is NOT by itself immutably limited. This matters, e.g. when
    --  checking the legality of an access to the current instance.
 
    function Is_Limited_View (Ent : Entity_Id) return Boolean;
@@ -301,7 +301,7 @@ package Sem_Aux is
    --  private type, limited interface type, task type, protected type,
    --  composite containing a limited component, or a subtype of any of
    --  these types). This older routine overlaps with the previous one, this
-   --  should be cleaned up?
+   --  should be cleaned up???
 
    function Nearest_Ancestor (Typ : Entity_Id) return Entity_Id;
    --  Given a subtype Typ, this function finds out the nearest ancestor from
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 6641f93..33f2407 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -20004,17 +20004,17 @@ package body Sem_Prag is
                         --  A state with a null refinement matches either a
                         --  null input list or nothing at all (no input):
 
-                        --    Refined_State (State => null)
+                        --    Refined_State   => (State => null)
 
                         --  No input
 
                         --    Depends         => (<output> => (State, Input))
-                        --    Refined_Depends => (<output> => Input  --  OK
+                        --    Refined_Depends => (<output> => Input)  --  OK
 
                         --  Null input list
 
                         --    Depends         => (<output> => State)
-                        --    Refined_Depends => (<output> => null)  --  OK
+                        --    Refined_Depends => (<output> => null)   --  OK
 
                         if Has_Null_Refinement (Dep_Id) then
                            Has_Null_State := True;
@@ -20073,6 +20073,20 @@ package body Sem_Prag is
 
                      Ref_Input := Next_Ref_Input;
                   end loop;
+
+                  --  When a state with a null refinement appears as the last
+                  --  input, it matches nothing:
+
+                  --    Refined_State   => (State => null)
+                  --    Depends         => (<output> => (Input, State))
+                  --    Refined_Depends => (<output> => Input)  --  OK
+
+                  if Ekind (Dep_Id) = E_Abstract_State
+                    and then Has_Null_Refinement (Dep_Id)
+                    and then No (Ref_Input)
+                  then
+                     Has_Null_State := True;
+                  end if;
                end if;
 
                --  A state with visible refinement was matched against one or