===================================================================
@@ -76,28 +76,35 @@
-- 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);
- return Get_Full_View (Non_Limited_View (Typ));
+ -- The non-limited view of an incomplete type may itself be incomplete
+ -- in which case obtain its full view.
- -- If it is class_wide, check whether the specific type comes from
- -- A limited_with.
+ elsif Is_Incomplete_Type (Ent)
+ and then Present (Non_Limited_View (Ent))
+ then
+ return Get_Full_View (Non_Limited_View (Ent));
- 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)))
+ -- If it is class_wide, check whether the specific type comes from a
+ -- limited_with.
+
+ 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;
===================================================================
@@ -90,12 +90,10 @@
-- 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
===================================================================
@@ -5385,31 +5385,36 @@
-------------------------
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 @@
-- 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');
- begin
-- 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 @@
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 @@
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 @@
end if;
end Decorate_Type;
- --------------------------
- -- Process_Declarations --
- --------------------------
+ -----------------------
+ -- Decorate_Variable --
+ -----------------------
- 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;
+ 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
+
+ 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 @@
-- 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 @@
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);
===================================================================
@@ -2497,7 +2497,8 @@
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 @@
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 @@
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 @@
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 =>
===================================================================
@@ -1316,10 +1316,11 @@
-- Freeze for further details.
-- From_Limited_With (Flag159)
+-- 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 @@
-- types if the modulus value is other than a power of 2.
-- Non_Limited_View (Node17)
+-- 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 @@
-- 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)
===================================================================
@@ -19905,7 +19905,7 @@
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,8 +19989,11 @@
-- 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 @@
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,14 +20379,18 @@
-- 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
-- A state with a null refinement matches either a null
-- output list or nothing at all (no clause):
- -- Refined_State => (State => null)
+ -- Refined_State => (State => null)
-- No clause
@@ -20446,6 +20465,18 @@
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 @@
-------------------------
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
===================================================================
@@ -5171,11 +5171,51 @@
-- 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 @@
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 @@
-- 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 @@
else
Error_Msg_N
("limited withed package can only be used to access "
- & "incomplete types",
- N);
+ & "incomplete types", N);
end if;
end if;
This patch implements abstract views of states and variables defined as: State abstractions are visible in the limited view of packages in SPARK 2014. The notion of an abstract view of a variable declaration is also introduced, and the limited view of a package includes the abstract view of any variables declared in the visible part of that package. The only allowed uses of an abstract view of a variable are where the use of a state abstraction would be allowed (for example, in a Global aspect_specification). A name denoting the abstract view of a variable shall occur only: * As a global_item in a Global or Refined_Global aspect specification; or * As an input or output in a Depends or Refined_Depends aspect specification. Any state abstractions declared within a given package are present in the limited view of the package. [This means that, for example, a Globals aspect_specification for a subprogram declared in a library unit package P1 could refer to a state abstraction declared in a package P2 if P1 has a limited with of P2.] For every variable object declared by an object_declaration occurring immediately within the visible part of a given package, the limited view of the package contains an abstract view of the object. ------------ -- Source -- ------------ -- lim_pack.ads package Lim_Pack with Abstract_State => ((In_State with External, Input_Only), (Out_State with External, Output_Only)) is In_Var : Integer; Out_Var : Integer; end Lim_Pack; -- pack.ads limited with Lim_Pack; package Pack with Abstract_State => (S1, S2) is procedure Proc (Formal : Integer) with Global => (Input => (Lim_Pack.In_State, Lim_Pack.In_Var, S1), Output => (Lim_Pack.Out_State, Lim_Pack.Out_Var, S2)), Depends => ((Lim_Pack.Out_State, Lim_Pack.Out_Var, S2) => (Lim_Pack.In_State, Lim_Pack.In_Var, S1, Formal)); end Pack; -- pack.adb with Lim_Pack; use Lim_Pack; package body Pack with Refined_State => (S1 => V1, S2 => V2) is V1 : Integer := 0; V2 : Integer := 0; procedure Proc (Formal : Integer) with Refined_Global => (Input => (In_State, In_Var, V1), Output => (Out_State, Out_Var, V2)), Refined_Depends => ((Out_State, Out_Var, V2) => (In_State, In_Var, V1, Formal)) is begin null; end Proc; end Pack; ----------------- -- Compilation -- ----------------- $ gcc -c -gnatd.V pack.adb Tested on x86_64-pc-linux-gnu, committed on trunk 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.