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.



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

1 files changed, 314 insertions, 70 deletions

diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index 69629419424..23083cddd88 100644
--- a/gcc/ada/sem_ch10.adb
+++ b/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));
-         Set_Ekind             (Shadow, Ekind (Ent));
+         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
-            Decorate_Type (Shadow, Scop, Is_Tagged);
+         --  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;
 
-      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;
-         Shadow      : Entity_Id;
-         Typ         : Entity_Id;
+            --  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
+
+         Is_Tagged : Boolean;
+         Decl      : Node_Id;
+         Def       : Node_Id;
+         Def_Id    : Entity_Id;
+         Shadow    : 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,
-                               N_Incomplete_Type_Declaration,
-                               N_Private_Extension_Declaration,
-                               N_Private_Type_Declaration,
-                               N_Protected_Type_Declaration,
-                               N_Task_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.
-
-               Shadow := Build_Shadow_Entity (Pack, Scop);
+               --  Create a shadow entity that hides the variable and offers an
+               --  abstract view of the said variable.
 
-               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);