einfo.adb (Non_Limited_View): Applies to abstract states.

2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb (Non_Limited_View): Applies to abstract states.
	(Set_From_Limited_With): Applies to abstract states.
	(Set_Non_Limited_View): Applies to abstract states.
	(Write_Field17): Output the non-limited view of an abstract state.
	* einfo.ads: Update the comment on usage and occurrences in
	nodes for attributes From_Limited_With and Non_Limited_View.
	* sem_aux.adb (Available_View): This routine can now handle
	abstract states.
	* sem_aux.ads (Available_View): This routine can now handle
	abstract states. Update the comment on usage.
	* sem_ch8.adb (Find_Expanded_Name): Handle abstract views
	of states and variables.
	(In_Pragmas_Depends_Or_Global): New routine.
	* sem_ch10.adb (Build_Limited_Views): Implement
	abstract (limited) views of variables and states.
	(Build_Shadow_Entity): This routine is now a procedure. Add
	formal parameter Shadow. Update the comment on usage. Add
	context-specific decoration for states and variables.
	(Decorate_State): New routine.	(Decorate_Variable): New routine.
	(Find_And_Process_States): New routine.
	(Process_Declarations): Renamed to Process_Declarations_And_States.
	(Process_Declarations_And_States): Add formal parameters
	Pack and Create_Abstract_Views. Update the comment on usage.
	(Process_States): New routine.
	* sem_prag.adb (Check_Dependency_Clause): Handle abstract
	views of states and variables. Match the abstract view of a state
	against its corresponding non-abstract view.
	(Is_Matching_Input):
	Handle abstract views of states and variables. Match the abstract
	view of a state against its corresponding non-abstract view.
	(Process_Global_Item): Handle abstract views of states and
	variables.

From-SVN: r206808

gcc/ada/ChangeLog

+2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* einfo.adb (Non_Limited_View): Applies to abstract states.
+	(Set_From_Limited_With): Applies to abstract states.
+	(Set_Non_Limited_View): Applies to abstract states.
+	(Write_Field17): Output the non-limited view of an abstract state.
+	* einfo.ads: Update the comment on usage and occurrences in
+	nodes for attributes From_Limited_With and Non_Limited_View.
+	* sem_aux.adb (Available_View): This routine can now handle
+	abstract states.
+	* sem_aux.ads (Available_View): This routine can now handle
+	abstract states. Update the comment on usage.
+	* sem_ch8.adb (Find_Expanded_Name): Handle abstract views
+	of states and variables.
+	(In_Pragmas_Depends_Or_Global): New routine.
+	* sem_ch10.adb (Build_Limited_Views): Implement
+	abstract (limited) views of variables and states.
+	(Build_Shadow_Entity): This routine is now a procedure. Add
+	formal parameter Shadow. Update the comment on usage. Add
+	context-specific decoration for states and variables.
+	(Decorate_State): New routine.	(Decorate_Variable): New routine.
+	(Find_And_Process_States): New routine.
+	(Process_Declarations): Renamed to Process_Declarations_And_States.
+	(Process_Declarations_And_States): Add formal parameters
+	Pack and Create_Abstract_Views. Update the comment on usage.
+	(Process_States): New routine.
+	* sem_prag.adb (Check_Dependency_Clause): Handle abstract
+	views of states and variables. Match the abstract view of a state
+	against its corresponding non-abstract view.
+	(Is_Matching_Input):
+	Handle abstract views of states and variables. Match the abstract
+	view of a state against its corresponding non-abstract view.
+	(Process_Global_Item): Handle abstract views of states and
+	variables.
+
 2014-01-20  Bob Duff  <duff@adacore.com>
 
 	* sem_ch10.adb (Expand_With_Clause): Don't

gcc/ada/einfo.adb

@@ -2497,7 +2497,8 @@ package body Einfo is
 
    function Non_Limited_View (Id : E) return E is
    begin
-      pragma Assert (Ekind (Id) in Incomplete_Kind);
+      pragma Assert
+        (Ekind (Id) in Incomplete_Kind or else Ekind (Id) = E_Abstract_State);
       return Node17 (Id);
    end Non_Limited_View;
 
@@ -3865,7 +3866,8 @@ package body Einfo is
 
    procedure Set_From_Limited_With (Id : E; V : B := True) is
    begin
-      pragma Assert (Is_Type (Id) or else Ekind (Id) = E_Package);
+      pragma Assert
+        (Is_Type (Id) or else Ekind_In (Id, E_Abstract_State, E_Package));
       Set_Flag159 (Id, V);
    end Set_From_Limited_With;
 
@@ -5172,7 +5174,8 @@ package body Einfo is
 
    procedure Set_Non_Limited_View (Id : E; V : E) is
    begin
-      pragma Assert (Ekind (Id) in Incomplete_Kind);
+      pragma Assert
+        (Ekind (Id) in Incomplete_Kind or else Ekind (Id) = E_Abstract_State);
       Set_Node17 (Id, V);
    end Set_Non_Limited_View;
 
@@ -8787,7 +8790,8 @@ package body Einfo is
          when Modular_Integer_Kind                         =>
             Write_Str ("Modulus");
 
-         when E_Incomplete_Type                            =>
+         when E_Abstract_State                             |
+              E_Incomplete_Type                            =>
             Write_Str ("Non_Limited_View");
 
          when E_Incomplete_Subtype                         =>

gcc/ada/einfo.ads

@@ -1316,10 +1316,11 @@ package Einfo is
 --       Freeze for further details.
 
 --    From_Limited_With (Flag159)
---       Defined in package and type entities. Set to True when the related
---       entity is generated by the expansion of a limited with clause. Such
---       an entity is said to be a "shadow" - it acts as the incomplete view
---       of a type by inheriting relevant attributes from the said type.
+--       Defined in abtract states, package and type entities. Set to True when
+--       the related entity is generated by the expansion of a limited with
+--       clause. Such an entity is said to be a "shadow" - it acts as the
+--       abstract view of a state or variable or as the incomplete view of a
+--       type by inheriting relevant attributes from the said entity.
 
 --    Full_View (Node11)
 --       Defined in all type and subtype entities and in deferred constants.
@@ -3262,9 +3263,9 @@ package Einfo is
 --       types if the modulus value is other than a power of 2.
 
 --    Non_Limited_View (Node17)
---       Defined in incomplete types that are the shadow entities created
---       when analyzing a limited_with_clause (Ada 2005: AI-50217). Points to
---       the defining entity in the original declaration.
+--       Defined in abstract states and incomplete types that act as shadow
+--       entities created when analysing a limited with clause (Ada 2005:
+--       AI-50217). Points to the defining entity of the original declaration.
 
 --    Nonzero_Is_True (Flag162) [base type only]
 --       Defined in enumeration types. Set if any non-zero value is to be
@@ -5120,6 +5121,8 @@ package Einfo is
    --    Refinement_Constituents             (Elist8)
    --    Refined_State                       (Node10)
    --    Body_References                     (Elist16)
+   --    Non_Limited_View                    (Node17)
+   --    From_Limited_With                   (Flag159)
    --    Has_Body_References                 (Flag264)
    --    Has_Visible_Refinement              (Flag263)
    --    Has_Non_Null_Refinement             (synth)

gcc/ada/sem_aux.adb

@@ -76,28 +76,35 @@ package body Sem_Aux is
    -- Available_View --
    --------------------
 
-   function Available_View (Typ : Entity_Id) return Entity_Id is
+   function Available_View (Ent : Entity_Id) return Entity_Id is
    begin
-      if Is_Incomplete_Type (Typ)
-        and then Present (Non_Limited_View (Typ))
+      --  Obtain the non-limited (non-abstract) view of a state or variable
+
+      if Ekind (Ent) = E_Abstract_State
+        and then Present (Non_Limited_View (Ent))
       then
-         --  The non-limited view may itself be an incomplete type, in which
-         --  case get its full view.
+         return Non_Limited_View (Ent);
+
+      --  The non-limited view of an incomplete type may itself be incomplete
+      --  in which case obtain its full view.
 
-         return Get_Full_View (Non_Limited_View (Typ));
+      elsif Is_Incomplete_Type (Ent)
+        and then Present (Non_Limited_View (Ent))
+      then
+         return Get_Full_View (Non_Limited_View (Ent));
 
-      --  If it is class_wide, check whether the specific type comes from
-      --  A limited_with.
+      --  If it is class_wide, check whether the specific type comes from a
+      --  limited_with.
 
-      elsif Is_Class_Wide_Type (Typ)
-        and then Is_Incomplete_Type (Etype (Typ))
-        and then From_Limited_With (Etype (Typ))
-        and then Present (Non_Limited_View (Etype (Typ)))
+      elsif Is_Class_Wide_Type (Ent)
+        and then Is_Incomplete_Type (Etype (Ent))
+        and then From_Limited_With (Etype (Ent))
+        and then Present (Non_Limited_View (Etype (Ent)))
       then
-         return Class_Wide_Type (Non_Limited_View (Etype (Typ)));
+         return Class_Wide_Type (Non_Limited_View (Etype (Ent)));
 
       else
-         return Typ;
+         return Ent;
       end if;
    end Available_View;
 

gcc/ada/sem_aux.ads

@@ -90,12 +90,10 @@ package Sem_Aux is
    --  subtype then it returns the subtype or type from which the subtype was
    --  obtained, otherwise it returns Empty.
 
-   function Available_View (Typ : Entity_Id) return Entity_Id;
-   --  Typ is typically a type that has the With_Type flag set. Returns the
-   --  non-limited view of the type, if available, otherwise the type itself.
-   --  For class-wide types, there is no direct link in the tree, so we have
-   --  to retrieve the class-wide type of the non-limited view of the Etype.
-   --  Returns the argument unchanged if it is not one of these cases.
+   function Available_View (Ent : Entity_Id) return Entity_Id;
+   --  Ent denotes an abstract state or a type that may come from a limited
+   --  with clause. Return the non-limited view of Ent if there is one or Ent
+   --  if this is not the case.
 
    function Constant_Value (Ent : Entity_Id) return Node_Id;
    --  Ent is a variable, constant, named integer, or named real entity. This

gcc/ada/sem_ch10.adb

@@ -5385,31 +5385,36 @@ package body Sem_Ch10 is
    -------------------------
 
    procedure Build_Limited_Views (N : Node_Id) is
-      Nam  : constant Node_Id          := Name (N);
-      Unum : constant Unit_Number_Type := Get_Source_Unit (Library_Unit (N));
-      Pack : constant Entity_Id        := Cunit_Entity (Unum);
+      Unum        : constant Unit_Number_Type :=
+                      Get_Source_Unit (Library_Unit (N));
+      Is_Analyzed : constant Boolean := Analyzed (Cunit (Unum));
 
       Shadow_Pack : Entity_Id;
       --  The corresponding shadow entity of the withed package. This entity
-      --  offers incomplete views of all types and visible packages declared
-      --  within.
+      --  offers incomplete views of packages and types as well as abstract
+      --  views of states and variables declared within.
 
       Last_Shadow : Entity_Id := Empty;
       --  The last shadow entity created by routine Build_Shadow_Entity
 
-      function Build_Shadow_Entity
+      procedure Build_Shadow_Entity
         (Ent       : Entity_Id;
          Scop      : Entity_Id;
-         Is_Tagged : Boolean := False) return Entity_Id;
-      --  Create a shadow entity that hides Ent and offers an incomplete view
-      --  of Ent. Scop is the proper scope. Flag Is_Tagged should be set when
-      --  Ent is a tagged type. The generated entity is added to Lim_Header.
-      --  This routine updates the value of Last_Shadow.
+         Shadow    : out Entity_Id;
+         Is_Tagged : Boolean := False);
+      --  Create a shadow entity that hides Ent and offers an abstract or
+      --  incomplete view of Ent. Scop is the proper scope. Flag Is_Tagged
+      --  should be set when Ent is a tagged type. The generated entity is
+      --  added to Lim_Header. This routine updates the value of Last_Shadow.
 
       procedure Decorate_Package (Ent : Entity_Id; Scop : Entity_Id);
       --  Perform minimal decoration of a package or its corresponding shadow
       --  entity denoted by Ent. Scop is the proper scope.
 
+      procedure Decorate_State (Ent : Entity_Id; Scop : Entity_Id);
+      --  Perform full decoration of an abstract state or its corresponding
+      --  shadow entity denoted by Ent. Scop is the proper scope.
+
       procedure Decorate_Type
         (Ent         : Entity_Id;
          Scop        : Entity_Id;
@@ -5421,28 +5426,47 @@ package body Sem_Ch10 is
       --  set when Ent is a tagged type and its class-wide type needs to appear
       --  in the tree.
 
-      procedure Process_Declarations (Decls : List_Id; Scop : Entity_Id);
-      --  Inspect declarative list Decls and create shadow entities for all
-      --  types and packages encountered. Scop is the proper scope.
+      procedure Decorate_Variable (Ent : Entity_Id; Scop : Entity_Id);
+      --  Perform minimal decoration of a variable denoted by Ent. Scop is the
+      --  proper scope.
+
+      procedure Process_Declarations_And_States
+        (Pack  : Entity_Id;
+         Decls : List_Id;
+         Scop  : Entity_Id;
+         Create_Abstract_Views : Boolean);
+      --  Inspect the states of package Pack and declarative list Decls. Create
+      --  shadow entities for all nested packages, states, types and variables
+      --  encountered. Scop is the proper scope. Create_Abstract_Views should
+      --  be set when the abstract states and variables need to be processed.
 
       -------------------------
       -- Build_Shadow_Entity --
       -------------------------
 
-      function Build_Shadow_Entity
+      procedure Build_Shadow_Entity
         (Ent       : Entity_Id;
          Scop      : Entity_Id;
-         Is_Tagged : Boolean := False) return Entity_Id
+         Shadow    : out Entity_Id;
+         Is_Tagged : Boolean := False)
       is
-         Shadow : constant Entity_Id := Make_Temporary (Sloc (Ent), 'Z');
-
       begin
+         Shadow := Make_Temporary (Sloc (Ent), 'Z');
+
          --  The shadow entity must share the same name and parent as the
          --  entity it hides.
 
          Set_Chars  (Shadow, Chars (Ent));
          Set_Parent (Shadow, Parent (Ent));
+
+         --  The abstract view of a variable is a state, not another variable
+
+         if Ekind (Ent) = E_Variable then
+            Set_Ekind (Shadow, E_Abstract_State);
+         else
             Set_Ekind (Shadow, Ekind (Ent));
+         end if;
+
          Set_Is_Internal       (Shadow);
          Set_From_Limited_With (Shadow);
 
@@ -5451,20 +5475,27 @@ package body Sem_Ch10 is
          Last_Shadow := Shadow;
          Append_Entity (Shadow, Shadow_Pack);
 
-         if Is_Type (Ent) then
+         --  Perform context-specific decoration of the shadow entity
+
+         if Ekind (Ent) = E_Abstract_State then
+            Decorate_State       (Shadow, Scop);
+            Set_Non_Limited_View (Shadow, Ent);
+
+         elsif Ekind (Ent) = E_Package then
+            Decorate_Package (Shadow, Scop);
+
+         elsif Is_Type (Ent) then
             Decorate_Type        (Shadow, Scop, Is_Tagged);
+            Set_Non_Limited_View (Shadow, Ent);
 
             if Is_Incomplete_Or_Private_Type (Ent) then
                Set_Private_Dependents (Shadow, New_Elmt_List);
             end if;
 
+         elsif Ekind (Ent) = E_Variable then
+            Decorate_State       (Shadow, Scop);
             Set_Non_Limited_View (Shadow, Ent);
-
-         elsif Ekind (Ent) = E_Package then
-            Decorate_Package (Shadow, Scop);
          end if;
-
-         return Shadow;
       end Build_Shadow_Entity;
 
       ----------------------
@@ -5478,6 +5509,19 @@ package body Sem_Ch10 is
          Set_Scope (Ent, Scop);
       end Decorate_Package;
 
+      --------------------
+      -- Decorate_State --
+      --------------------
+
+      procedure Decorate_State (Ent : Entity_Id; Scop : Entity_Id) is
+      begin
+         Set_Ekind                   (Ent, E_Abstract_State);
+         Set_Etype                   (Ent, Standard_Void_Type);
+         Set_Scope                   (Ent, Scop);
+         Set_Refined_State           (Ent, Empty);
+         Set_Refinement_Constituents (Ent, New_Elmt_List);
+      end Decorate_State;
+
       -------------------
       -- Decorate_Type --
       -------------------
@@ -5540,36 +5584,229 @@ package body Sem_Ch10 is
          end if;
       end Decorate_Type;
 
-      --------------------------
-      -- Process_Declarations --
-      --------------------------
+      -----------------------
+      -- Decorate_Variable --
+      -----------------------
+
+      procedure Decorate_Variable (Ent : Entity_Id; Scop : Entity_Id) is
+      begin
+         Set_Ekind (Ent, E_Variable);
+         Set_Etype (Ent, Standard_Void_Type);
+         Set_Scope (Ent, Scop);
+      end Decorate_Variable;
+
+      -------------------------------------
+      -- Process_Declarations_And_States --
+      -------------------------------------
+
+      procedure Process_Declarations_And_States
+        (Pack  : Entity_Id;
+         Decls : List_Id;
+         Scop  : Entity_Id;
+         Create_Abstract_Views : Boolean)
+      is
+         procedure Find_And_Process_States;
+         --  Determine whether package Pack defines abstract state either by
+         --  using an aspect or a pragma. If this is the case, build shadow
+         --  entities for all abstract states of Pack.
+
+         procedure Process_States (States : Elist_Id);
+         --  Generate shadow entities for all abstract states in list States
+
+         -----------------------------
+         -- Find_And_Process_States --
+         -----------------------------
+
+         procedure Find_And_Process_States is
+            procedure Process_State (State : Node_Id);
+            --  Generate shadow entities for a single abstract state or
+            --  multiple states expressed as an aggregate.
+
+            -------------------
+            -- Process_State --
+            -------------------
+
+            procedure Process_State (State : Node_Id) is
+               Loc  : constant Source_Ptr := Sloc (State);
+               Elmt : Node_Id;
+               Id   : Entity_Id;
+               Name : Name_Id;
+
+               Dummy : Entity_Id;
+               pragma Unreferenced (Dummy);
+
+            begin
+               --  Multiple abstract states appear as an aggregate
+
+               if Nkind (State) = N_Aggregate then
+                  Elmt := First (Expressions (State));
+                  while Present (Elmt) loop
+                     Process_State (Elmt);
+
+                     Next (Elmt);
+                  end loop;
+                  return;
+
+               --  A null state has no abstract view
+
+               elsif Nkind (State) = N_Null then
+                  return;
+
+               --  State declaration with various options appears as an
+               --  extension aggregate.
+
+               elsif Nkind (State) = N_Extension_Aggregate then
+                  Name := Chars (Ancestor_Part (State));
+
+               --  Simple state declaration
+
+               elsif Nkind (State) = N_Identifier then
+                  Name := Chars (State);
+
+               --  Possibly an illegal state declaration
+
+               else
+                  return;
+               end if;
+
+               --  Construct a dummy state for the purposes of establishing a
+               --  non-limited => limited view relation. Note that the dummy
+               --  state is not added to list Abstract_States to avoid multiple
+               --  definitions.
+
+               Id := Make_Defining_Identifier (Loc, New_External_Name (Name));
+               Set_Parent     (Id, State);
+               Decorate_State (Id, Scop);
+
+               Build_Shadow_Entity (Id, Scop, Dummy);
+            end Process_State;
+
+            --  Local variables
+
+            Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack);
+            Asp       : Node_Id;
+            Decl      : Node_Id;
+
+         --  Start of processing for Find_And_Process_States
+
+         begin
+            --  Find aspect Abstract_State
+
+            Asp := First (Aspect_Specifications (Pack_Decl));
+            while Present (Asp) loop
+               if Chars (Identifier (Asp)) = Name_Abstract_State then
+                  Process_State (Expression (Asp));
+
+                  return;
+               end if;
+
+               Next (Asp);
+            end loop;
+
+            --  Find pragma Abstract_State by inspecting the declarations
+
+            Decl := First (Decls);
+            while Present (Decl) and then Nkind (Decl) = N_Pragma loop
+               if Pragma_Name (Decl) = Name_Abstract_State then
+                  Process_State
+                    (Get_Pragma_Arg
+                       (First (Pragma_Argument_Associations (Decl))));
+
+                  return;
+               end if;
+
+               Next (Decl);
+            end loop;
+         end Find_And_Process_States;
+
+         --------------------
+         -- Process_States --
+         --------------------
+
+         procedure Process_States (States : Elist_Id) is
+            Dummy : Entity_Id;
+            Elmt  : Elmt_Id;
+
+         begin
+            Elmt := First_Elmt (States);
+            while Present (Elmt) loop
+               Build_Shadow_Entity (Node (Elmt), Scop, Dummy);
+
+               Next_Elmt (Elmt);
+            end loop;
+         end Process_States;
+
+         --  Local variables
 
-      procedure Process_Declarations (Decls : List_Id; Scop : Entity_Id) is
-         Is_Analyzed : constant Boolean := Analyzed (Cunit (Unum));
          Is_Tagged : Boolean;
          Decl      : Node_Id;
          Def       : Node_Id;
-         Pack        : Entity_Id;
+         Def_Id    : Entity_Id;
          Shadow    : Entity_Id;
-         Typ         : Entity_Id;
+
+      --  Start of processing for Process_Declarations_And_States
 
       begin
-         --  Inspect the declarative list, looking for type declarations and
-         --  nested packages.
+         --  Build abstract views for all states defined in the package
+
+         if Create_Abstract_Views then
+
+            --  When a package has been analyzed, all states are stored in list
+            --  Abstract_States. Generate the shadow entities directly.
+
+            if Is_Analyzed then
+               if Present (Abstract_States (Pack)) then
+                  Process_States (Abstract_States (Pack));
+               end if;
+
+            --  The package may declare abstract states by using an aspect or a
+            --  pragma. Attempt to locate one of these construct and if found,
+            --  build the shadow entities.
+
+            else
+               Find_And_Process_States;
+            end if;
+         end if;
+
+         --  Inspect the declarative list, looking for nested packages, types
+         --  and variable declarations.
 
          Decl := First (Decls);
          while Present (Decl) loop
 
+            --  Packages
+
+            if Nkind (Decl) = N_Package_Declaration then
+               Def_Id := Defining_Entity (Decl);
+
+               --  Perform minor decoration when the withed package has not
+               --  been analyzed.
+
+               if not Is_Analyzed then
+                  Decorate_Package (Def_Id, Scop);
+               end if;
+
+               --  Create a shadow entity that offers a limited view of all
+               --  visible types declared within.
+
+               Build_Shadow_Entity (Def_Id, Scop, Shadow);
+
+               Process_Declarations_And_States
+                 (Pack  => Def_Id,
+                  Decls => Visible_Declarations (Specification (Decl)),
+                  Scop  => Shadow,
+                  Create_Abstract_Views => Create_Abstract_Views);
+
             --  Types
 
-            if Nkind_In (Decl, N_Full_Type_Declaration,
+            elsif Nkind_In (Decl, N_Full_Type_Declaration,
                                   N_Incomplete_Type_Declaration,
                                   N_Private_Extension_Declaration,
                                   N_Private_Type_Declaration,
                                   N_Protected_Type_Declaration,
                                   N_Task_Type_Declaration)
             then
-               Typ := Defining_Entity (Decl);
+               Def_Id := Defining_Entity (Decl);
 
                --  Determine whether the type is tagged. Note that packages
                --  included via a limited with clause are not always analyzed,
@@ -5602,42 +5839,44 @@ package body Sem_Ch10 is
                --  been analyzed.
 
                if not Is_Analyzed then
-                  Decorate_Type (Typ, Scop, Is_Tagged, True);
+                  Decorate_Type (Def_Id, Scop, Is_Tagged, True);
                end if;
 
                --  Create a shadow entity that hides the type and offers an
                --  incomplete view of the said type.
 
-               Shadow := Build_Shadow_Entity (Typ, Scop, Is_Tagged);
+               Build_Shadow_Entity (Def_Id, Scop, Shadow, Is_Tagged);
 
-            --  Packages
+            --  Variables
 
-            elsif Nkind (Decl) = N_Package_Declaration then
-               Pack := Defining_Entity (Decl);
+            elsif Create_Abstract_Views
+              and then Nkind (Decl) = N_Object_Declaration
+              and then not Constant_Present (Decl)
+            then
+               Def_Id := Defining_Entity (Decl);
 
                --  Perform minor decoration when the withed package has not
                --  been analyzed.
 
                if not Is_Analyzed then
-                  Decorate_Package (Pack, Scop);
+                  Decorate_Variable (Def_Id, Scop);
                end if;
 
-               --  Create a shadow entity that offers a limited view of all
-               --  visible types declared within.
+               --  Create a shadow entity that hides the variable and offers an
+               --  abstract view of the said variable.
 
-               Shadow := Build_Shadow_Entity (Pack, Scop);
-
-               Process_Declarations
-                 (Decls => Visible_Declarations (Specification (Decl)),
-                  Scop  => Shadow);
+               Build_Shadow_Entity (Def_Id, Scop, Shadow);
             end if;
 
             Next (Decl);
          end loop;
-      end Process_Declarations;
+      end Process_Declarations_And_States;
 
       --  Local variables
 
+      Nam  : constant Node_Id   := Name (N);
+      Pack : constant Entity_Id := Cunit_Entity (Unum);
+
       Last_Public_Shadow : Entity_Id := Empty;
       Private_Shadow     : Entity_Id;
       Spec               : Node_Id;
@@ -5719,21 +5958,26 @@ package body Sem_Ch10 is
       Set_Is_Internal  (Shadow_Pack);
       Set_Limited_View (Pack, Shadow_Pack);
 
-      --  Inspect the visible declarations of the withed unit and create shadow
-      --  entities that hide existing types and packages.
+      --  Inspect the abstract states and visible declarations of the withed
+      --  unit and create shadow entities that hide existing packages, states,
+      --  variables and types.
 
-      Process_Declarations
-        (Decls => Visible_Declarations (Spec),
-         Scop  => Pack);
+      Process_Declarations_And_States
+        (Pack  => Pack,
+         Decls => Visible_Declarations (Spec),
+         Scop  => Pack,
+         Create_Abstract_Views => True);
 
       Last_Public_Shadow := Last_Shadow;
 
       --  Ada 2005 (AI-262): Build the limited view of the private declarations
       --  to accomodate limited private with clauses.
 
-      Process_Declarations
-        (Decls => Private_Declarations (Spec),
-         Scop  => Pack);
+      Process_Declarations_And_States
+        (Pack  => Pack,
+         Decls => Private_Declarations (Spec),
+         Scop  => Pack,
+         Create_Abstract_Views => False);
 
       if Present (Last_Public_Shadow) then
          Private_Shadow := Next_Entity (Last_Public_Shadow);

gcc/ada/sem_ch8.adb

@@ -5171,11 +5171,51 @@ package body Sem_Ch8 is
    --  the scope of its declaration.
 
    procedure Find_Expanded_Name (N : Node_Id) is
+      function In_Pragmas_Depends_Or_Global (N : Node_Id) return Boolean;
+      --  Determine whether an arbitrary node N appears in pragmas [Refined_]
+      --  Depends or [Refined_]Global.
+
+      ----------------------------------
+      -- In_Pragmas_Depends_Or_Global --
+      ----------------------------------
+
+      function In_Pragmas_Depends_Or_Global (N : Node_Id) return Boolean is
+         Par : Node_Id;
+
+      begin
+         --  Climb the parent chain looking for a pragma
+
+         Par := N;
+         while Present (Par) loop
+            if Nkind (Par) = N_Pragma
+              and then Nam_In (Pragma_Name (Par), Name_Depends,
+                                                  Name_Global,
+                                                  Name_Refined_Depends,
+                                                  Name_Refined_Global)
+            then
+               return True;
+
+            --  Prevent the search from going too far
+
+            elsif Is_Body_Or_Package_Declaration (Par) then
+               return False;
+            end if;
+
+            Par := Parent (Par);
+         end loop;
+
+         return False;
+      end In_Pragmas_Depends_Or_Global;
+
+      --  Local variables
+
       Selector  : constant Node_Id := Selector_Name (N);
       Candidate : Entity_Id        := Empty;
       P_Name    : Entity_Id;
       Id        : Entity_Id;
 
+   --  Start of processing for Find_Expanded_Name
+
    begin
       P_Name := Entity (Prefix (N));
 
@@ -5210,6 +5250,27 @@ package body Sem_Ch8 is
                Candidate        := Id;
                Is_New_Candidate := True;
 
+               --  Handle abstract views of states and variables. These are
+               --  acceptable only when the reference to the view appears in
+               --  pragmas [Refined_]Depends and [Refined_]Global.
+
+               if Ekind (Id) = E_Abstract_State
+                 and then From_Limited_With (Id)
+                 and then Present (Non_Limited_View (Id))
+               then
+                  if In_Pragmas_Depends_Or_Global (N) then
+                     Candidate        := Non_Limited_View (Id);
+                     Is_New_Candidate := True;
+
+                  --  Hide the candidate because it is not used in a proper
+                  --  context.
+
+                  else
+                     Candidate        := Empty;
+                     Is_New_Candidate := False;
+                  end if;
+               end if;
+
             --  Ada 2005 (AI-217): Handle shadow entities associated with types
             --  declared in limited-withed nested packages. We don't need to
             --  handle E_Incomplete_Subtype entities because the entities in
@@ -5221,9 +5282,8 @@ package body Sem_Ch8 is
             --  The non-limited view may itself be incomplete, in which case
             --  get the full view if available.
 
-            elsif From_Limited_With (Id)
-              and then Is_Type (Id)
-              and then Ekind (Id) = E_Incomplete_Type
+            elsif Ekind (Id) = E_Incomplete_Type
+              and then From_Limited_With (Id)
               and then Present (Non_Limited_View (Id))
               and then Scope (Non_Limited_View (Id)) = P_Name
             then
@@ -5528,8 +5588,7 @@ package body Sem_Ch8 is
          else
             Error_Msg_N
               ("limited withed package can only be used to access "
-               & "incomplete types",
-                N);
+               & "incomplete types", N);
          end if;
       end if;
 

gcc/ada/sem_prag.adb

@@ -19905,7 +19905,7 @@ package body Sem_Prag is
          function Output_Constituents (State_Id : Entity_Id) return Elist_Id;
          --  Given a state denoted by State_Id, return a list of all output
          --  constituents that may be referenced within Refined_Depends. The
-         --  contents of the list depend on whethe Refined_Global is present.
+         --  contents of the list depend on whether Refined_Global is present.
 
          procedure Report_Unused_Constituents (Constits : Elist_Id);
          --  Emit errors for all constituents found in list Constits
@@ -19989,7 +19989,10 @@ package body Sem_Prag is
                --  Remaining cases are formal parameters, variables, and states
 
                else
-                  Dep_Id := Entity_Of (Dep_Input);
+                  --  Handle abstract views of states and variables generated
+                  --  for limited with clauses.
+
+                  Dep_Id := Available_View (Entity_Of (Dep_Input));
 
                   --  Inspect all inputs of the refinement clause and attempt
                   --  to match against the inputs of the dependence clause.
@@ -20061,6 +20064,18 @@ package body Sem_Prag is
                                  Remove (Ref_Input);
                               end if;
                            end if;
+
+                        --  The abstract view of a state matches its
+                        --  corresponding non-abstract view:
+
+                        --    Depends         => (<output> => Lim_Pack.State)
+                        --    Refined_Depends => (<output> => State)
+
+                        elsif Is_Entity_Name (Ref_Input)
+                          and then Entity_Of (Ref_Input) = Dep_Id
+                        then
+                           Remove (Ref_Input);
+                           return True;
                         end if;
 
                      --  Formal parameters and variables are matched on
@@ -20364,7 +20379,11 @@ package body Sem_Prag is
             --  The remaining cases are formal parameters, variables and states
 
             elsif Is_Entity_Name (Dep_Output) then
-               Dep_Id := Entity_Of (Dep_Output);
+
+               --  Handle abstract views of states and variables generated for
+               --  limited with clauses.
+
+               Dep_Id := Available_View (Entity_Of (Dep_Output));
 
                if Ekind (Dep_Id) = E_Abstract_State then
 
@@ -20446,6 +20465,18 @@ package body Sem_Prag is
                            Remove (Out_Constits, Ref_Id);
                         end if;
                      end if;
+
+                  --  The abstract view of a state matches is corresponding
+                  --  non-abstract view:
+
+                  --    Depends         => (Lim_Pack.State => <input>)
+                  --    Refined_Depends => (State          => <input>)
+
+                  elsif Is_Entity_Name (Ref_Output)
+                    and then Entity_Of (Ref_Output) = Dep_Id
+                  then
+                     Matching_Clause := Ref_Clause;
+                     exit;
                   end if;
 
                --  Formal parameters and variables match if their inputs match
@@ -22127,7 +22158,9 @@ package body Sem_Prag is
          -------------------------
 
          procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id) is
-            Item_Id : constant Entity_Id := Entity_Of (Item);
+            Item_Id : constant Entity_Id := Available_View (Entity_Of (Item));
+            --  The above handles abstract views of variables and states built
+            --  for limited with clauses.
 
          begin
             --  Signal that the global list contains at least one abstract