+2016-10-12 Ed Schonberg <schonberg@adacore.com>
+
+ * lib-writ.adb (Write_ALI): Removal of unused file entries from
+ dependency list must be performed before the list is sorted,
+ so that the dependency number of other files is properly set-up
+ for use in tools that relate entity information to the unit in
+ which they are declared.
+
+2016-10-12 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_aggr.adb (Initialize_Ctrl_Array_Component):
+ Create a copy of the initialization expression to avoid sharing
+ it between multiple components.
+
+2016-10-12 Yannick Moy <moy@adacore.com>
+
+ * einfo.adb, einfo.ads (Has_Partial_Visible_Refinement): New flag
+ in abtract states.
+ (Has_Non_Null_Visible_Refinement): Return true for patial refinement.
+ (Partial_Refinement_Constituents): New function returns the full or
+ partial refinement constituents depending on scope.
+ * sem_ch3.adb (Analyze_Declarations): Remove partial visible
+ refinements when exiting the scope of a package spec or body
+ and those partial refinements are not in scope afterwards.
+ * sem_ch7.adb, sem_ch7.ads (Install_Partial_Declarations): Mark
+ abstract states of parent units with partial refinement so that
+ it is visible.
+ * sem_prag.adb (Analyze_Part_Of_In_Decl_Part): Mark enclosing
+ abstract state if any as having partial refinement in that scope.
+ (Analyze_Refined_Global_In_Decl_Part): Check constituent usage
+ based on full or partial refinement depending on scope.
+
+2016-10-12 Ed Schonberg <schonberg@adacore.com>
+
+ * exp_ch4.adb (Expand_N_Type_Conversion): If the target type
+ has an invariant aspect, insert invariant call at the proper
+ place in the code rather than rewriting the expression as an
+ expression with actions, to prevent spurious semantic errors on
+ the rewritten conversion when it is the object in a renaming.
+
2016-10-12 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch5.adb, sem_ch3.adb, exp_ch9.adb, a-tags.adb, sem_prag.adb,
-- Is_Actual_Subtype Flag293
-- Has_Pragma_Unused Flag294
-- Is_Ignored_Transient Flag295
+ -- Has_Partial_Visible_Refinement Flag296
- -- (unused) Flag296
-- (unused) Flag297
-- (unused) Flag298
-- (unused) Flag299
return Flag232 (Id);
end Has_Own_Invariants;
+ function Has_Partial_Visible_Refinement (Id : E) return B is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ return Flag296 (Id);
+ end Has_Partial_Visible_Refinement;
+
function Has_Per_Object_Constraint (Id : E) return B is
begin
return Flag154 (Id);
Set_Flag232 (Id, V);
end Set_Has_Own_Invariants;
+ procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True) is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Set_Flag296 (Id, V);
+ end Set_Has_Partial_Visible_Refinement;
+
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True) is
begin
Set_Flag154 (Id, V);
pragma Assert (Ekind (Id) = E_Abstract_State);
Constits := Refinement_Constituents (Id);
- -- For a refinement to be non-null, the first constituent must be
- -- anything other than null.
+ -- A partial refinement is always non-null. For a full refinement to be
+ -- non-null, the first constituent must be anything other than null.
return
- Has_Visible_Refinement (Id)
- and then Present (Constits)
- and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
+ Has_Partial_Visible_Refinement (Id)
+ or else (Has_Visible_Refinement (Id)
+ and then Present (Constits)
+ and then Nkind (Node (First_Elmt (Constits))) /= N_Null);
end Has_Non_Null_Visible_Refinement;
-----------------------------
return Empty;
end Partial_Invariant_Procedure;
+ -------------------------------------
+ -- Partial_Refinement_Constituents --
+ -------------------------------------
+
+ function Partial_Refinement_Constituents (Id : E) return L is
+ Constits : Elist_Id;
+
+ begin
+ -- "Refinement" is a concept applicable only to abstract states
+
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Constits := Refinement_Constituents (Id);
+
+ -- A refinement may be partially visible when objects declared in the
+ -- private part of a package are subject to a Part_Of indicator.
+
+ if No (Constits) then
+ Constits := Part_Of_Constituents (Id);
+ end if;
+
+ return Constits;
+ end Partial_Refinement_Constituents;
+
------------------------
-- Predicate_Function --
------------------------
-- one invariant of its own. The flag is also set on the full view of a
-- private extension or a private type for completeness.
+-- Has_Partial_Visible_Refinement (Flag296)
+-- Defined in E_Abstract_State entities. Set when a state has at least
+-- one refinement constituent subject to indicator Part_Of, and analysis
+-- is in the region between the declaration of the first constituent for
+-- this abstract state (in the private part of the package) and the end
+-- of the package spec or body with visibility over this private part
+-- (which includes the package itself and its child packages).
+
-- Has_Per_Object_Constraint (Flag154)
-- Defined in E_Component entities. Set if the subtype of the component
-- has a per object constraint. Per object constraints result from the
-- Note: the reason this is marked as a synthesized attribute is that the
-- way this is stored is as an element of the Subprograms_For_Type field.
+-- Partial_Refinement_Constituents (synthesized)
+-- Present in abstract state entities. Contains the constituents that
+-- refine the state in its private part, in other words, all the hidden
+-- states that indicate this abstract state in a Part_Of aspect/pragma.
+
-- Partial_View_Has_Unknown_Discr (Flag280)
-- Present in all types. Set to Indicate that the partial view of a type
-- has unknown discriminants. A default initialization of an object of
-- Non_Limited_View (Node19)
-- Encapsulating_State (Node32)
-- From_Limited_With (Flag159)
+ -- Has_Partial_Visible_Refinement (Flag296)
-- Has_Visible_Refinement (Flag263)
-- Has_Non_Limited_View (synth)
-- Has_Non_Null_Visible_Refinement (synth)
-- Is_External_State (synth)
-- Is_Null_State (synth)
-- Is_Synchronized_State (synth)
+ -- Partial_Refinement_Constituents (synth)
-- E_Access_Protected_Subprogram_Type
-- Equivalent_Type (Node18)
function Has_Object_Size_Clause (Id : E) return B;
function Has_Out_Or_In_Out_Parameter (Id : E) return B;
function Has_Own_Invariants (Id : E) return B;
+ function Has_Partial_Visible_Refinement (Id : E) return B;
function Has_Per_Object_Constraint (Id : E) return B;
function Has_Pragma_Controlled (Id : E) return B;
function Has_Pragma_Elaborate_Body (Id : E) return B;
function Number_Entries (Id : E) return Nat;
function Number_Formals (Id : E) return Pos;
function Parameter_Mode (Id : E) return Formal_Kind;
+ function Partial_Refinement_Constituents (Id : E) return L;
function Primitive_Operations (Id : E) return L;
function Root_Type (Id : E) return E;
function Safe_Emax_Value (Id : E) return U;
procedure Set_Has_Object_Size_Clause (Id : E; V : B := True);
procedure Set_Has_Out_Or_In_Out_Parameter (Id : E; V : B := True);
procedure Set_Has_Own_Invariants (Id : E; V : B := True);
+ procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True);
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True);
procedure Set_Has_Pragma_Controlled (Id : E; V : B := True);
procedure Set_Has_Pragma_Elaborate_Body (Id : E; V : B := True);
pragma Inline (Has_Object_Size_Clause);
pragma Inline (Has_Out_Or_In_Out_Parameter);
pragma Inline (Has_Own_Invariants);
+ pragma Inline (Has_Partial_Visible_Refinement);
pragma Inline (Has_Per_Object_Constraint);
pragma Inline (Has_Pragma_Controlled);
pragma Inline (Has_Pragma_Elaborate_Body);
pragma Inline (Set_Has_Object_Size_Clause);
pragma Inline (Set_Has_Out_Or_In_Out_Parameter);
pragma Inline (Set_Has_Own_Invariants);
+ pragma Inline (Set_Has_Partial_Visible_Refinement);
pragma Inline (Set_Has_Per_Object_Constraint);
pragma Inline (Set_Has_Pragma_Controlled);
pragma Inline (Set_Has_Pragma_Elaborate_Body);
is
Act_Aggr : Node_Id;
Act_Stmts : List_Id;
+ Expr : Node_Id;
Fin_Call : Node_Id;
Hook_Clear : Node_Id;
-- in-place expansion.
begin
+ -- Duplicate the initialization expression in case the context is
+ -- a multi choice list or an "others" choice which plugs various
+ -- holes in the aggregate. As a result the expression is no longer
+ -- shared between the various components and is reevaluated for
+ -- each such component.
+
+ Expr := New_Copy_Tree (Init_Expr);
+ Set_Parent (Expr, Parent (Init_Expr));
+
-- Perform a preliminary analysis and resolution to determine what
-- the initialization expression denotes. An unanalyzed function
-- call may appear as an identifier or an indexed component.
- if Nkind_In (Init_Expr, N_Function_Call,
- N_Identifier,
- N_Indexed_Component)
- and then not Analyzed (Init_Expr)
+ if Nkind_In (Expr, N_Function_Call,
+ N_Identifier,
+ N_Indexed_Component)
+ and then not Analyzed (Expr)
then
- Preanalyze_And_Resolve (Init_Expr, Comp_Typ);
+ Preanalyze_And_Resolve (Expr, Comp_Typ);
end if;
In_Place_Expansion :=
- Nkind (Init_Expr) = N_Function_Call
+ Nkind (Expr) = N_Function_Call
and then not Is_Limited_Type (Comp_Typ);
-- The initialization expression is a controlled function call.
-- generation of a transient scope, which leads to out-of-order
-- adjustment and finalization.
- Set_No_Side_Effect_Removal (Init_Expr);
+ Set_No_Side_Effect_Removal (Expr);
-- When the transient component initialization is related to a
-- range or an "others", keep all generated statements within
Process_Transient_Component
(Loc => Loc,
Comp_Typ => Comp_Typ,
- Init_Expr => Init_Expr,
+ Init_Expr => Expr,
Fin_Call => Fin_Call,
Hook_Clear => Hook_Clear,
Aggr => Act_Aggr,
Initialize_Array_Component
(Arr_Comp => Arr_Comp,
Comp_Typ => Comp_Typ,
- Init_Expr => Init_Expr,
+ Init_Expr => Expr,
Stmts => Stmts);
-- At this point the array element is fully initialized. Complete
end if;
-- Check for case of converting to a type that has an invariant
- -- associated with it. This required an invariant check. We convert
+ -- associated with it. This requires an invariant check. We insert
+ -- a call:
- -- typ (expr)
+ -- invariant_check (typ (expr))
- -- into
-
- -- do invariant_check (typ (expr)) in typ (expr);
-
- -- using Duplicate_Subexpr to avoid multiple side effects
+ -- in the code, after removing side effects from the expression.
+ -- This is clearer than replacing the conversion into an expression
+ -- with actions, because the context may impose additional actions
+ -- (tag checks, membership tests, etc.) that conflict with this
+ -- rewriting (used previously).
-- Note: the Comes_From_Source check, and then the resetting of this
-- flag prevents what would otherwise be an infinite recursion.
and then Comes_From_Source (N)
then
Set_Comes_From_Source (N, False);
- Rewrite (N,
- Make_Expression_With_Actions (Loc,
- Actions => New_List (
- Make_Invariant_Call (Duplicate_Subexpr (N))),
- Expression => Duplicate_Subexpr_No_Checks (N)));
- Analyze_And_Resolve (N, Target_Type);
+ Remove_Side_Effects (N);
+ Insert_Action (N, Make_Invariant_Call (Duplicate_Subexpr (N)));
goto Done;
end if;
if Cunit_Entity (Unum) = Empty
or else not From_Limited_With (Cunit_Entity (Unum))
then
- Num_Sdep := Num_Sdep + 1;
- Sdep_Table (Num_Sdep) := Unum;
+ -- Units that are not analyzed need not appear in the dependency
+ -- list. These units are either units appearing in limited_with
+ -- clauses of other units, or units loaded for inlining that end
+ -- up not inlined by a later decision of the inlining code, to
+ -- prevent circularities. We want to exclude these files from the
+ -- list of dependencies, so that the dependency number of other
+ -- is correctly set, as that number is used by cross-reference
+ -- tools to relate entity information to the unit in which they
+ -- are declared.
+
+ if Present (Cunit_Entity (Unum))
+ and then Ekind (Cunit_Entity (Unum)) = E_Void
+ and then Nkind (Unit (Cunit (Unum))) /= N_Subunit
+ and then Serious_Errors_Detected = 0
+ then
+ null;
+
+ else
+ Num_Sdep := Num_Sdep + 1;
+ Sdep_Table (Num_Sdep) := Unum;
+ end if;
end if;
end loop;
Units.Table (Unum).Dependency_Num := J;
Sind := Units.Table (Unum).Source_Index;
- -- The dependency table also contains units that appear in the
- -- context of a unit loaded through a limited_with clause. These
- -- units are never analyzed, and thus the main unit does not
- -- really have a dependency on them. Subunits are always compiled
- -- in the context of the parent, and their file table entries are
- -- not properly decorated, they are recognized syntactically.
-
- -- This optimization is disabled when inline is active, because
- -- inline may propose some bodies for inlining, and decide later
- -- that they may lead to circularities, in which case they are
- -- also left unanalyzed in the file table. There is no simple way
- -- to distinguish between the two kinds of unanalyzed entries,
- -- so simplest is to skip this step.
-
- -- Actually, this optimization is always disabled, because it
- -- breaks gnatfind.
-
- if False -- ???
- and then Present (Cunit_Entity (Unum))
- and then Ekind (Cunit_Entity (Unum)) = E_Void
- and then Nkind (Unit (Cunit (Unum))) /= N_Subunit
- and then not Inline_Active
- then
- goto Next_Unit;
- end if;
-
Write_Info_Initiate ('D');
Write_Info_Char (' ');
end if;
Write_Info_EOL;
-
- <<Next_Unit>>
- null;
end loop;
end;
-- case, add a proper spec if the body lacks one. The spec is inserted
-- before Body_Decl and immediately analyzed.
+ procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id);
+ -- Spec_Id is the entity of a package that may define abstract states,
+ -- and in the case of a child unit, whose ancestors may define abstract
+ -- states. If the states have partial visible refinement, remove the
+ -- partial visibility of each constituent at the end of the package
+ -- spec and body declarations.
+
procedure Remove_Visible_Refinements (Spec_Id : Entity_Id);
-- Spec_Id is the entity of a package that may define abstract states.
-- If the states have visible refinement, remove the visibility of each
- -- constituent at the end of the package body declarations.
+ -- constituent at the end of the package body declaration.
-----------------
-- Adjust_Decl --
Insert_Before_And_Analyze (Body_Decl, Decl);
end Handle_Late_Controlled_Primitive;
+ ----------------------------------------
+ -- Remove_Partial_Visible_Refinements --
+ ----------------------------------------
+
+ procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id) is
+ State_Elmt : Elmt_Id;
+ begin
+ if Present (Abstract_States (Spec_Id)) then
+ State_Elmt := First_Elmt (Abstract_States (Spec_Id));
+ while Present (State_Elmt) loop
+ Set_Has_Partial_Visible_Refinement (Node (State_Elmt), False);
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+
+ -- For a child unit, also hide the partial state refinement from
+ -- ancestor packages.
+
+ if Is_Child_Unit (Spec_Id) then
+ Remove_Partial_Visible_Refinements (Scope (Spec_Id));
+ end if;
+ end Remove_Partial_Visible_Refinements;
+
--------------------------------
-- Remove_Visible_Refinements --
--------------------------------
-- restore the original state conditions.
Remove_Visible_Refinements (Corresponding_Spec (Context));
+ Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
+
+ elsif Nkind (Context) = N_Package_Declaration then
+
+ -- Partial state refinements are visible up to the end of the
+ -- package spec declarations. Hide the partial state refinements
+ -- from visibility to restore the original state conditions.
+
+ Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
end if;
-- Verify that all abstract states found in any package declared in
Next_Entity (Id);
end loop;
+ -- An abstract state is partially refined when it has at least one
+ -- Part_Of constituent. Since these constituents are being installed
+ -- into visibility, update the partial refinement status of any state
+ -- defined in the associated package, subject to at least one Part_Of
+ -- constituent.
+
+ if Ekind_In (P, E_Generic_Package, E_Package) then
+ declare
+ States : constant Elist_Id := Abstract_States (P);
+ State_Elmt : Elmt_Id;
+ State_Id : Entity_Id;
+
+ begin
+ if Present (States) then
+ State_Elmt := First_Elmt (States);
+ while Present (State_Elmt) loop
+ State_Id := Node (State_Elmt);
+
+ if Present (Part_Of_Constituents (State_Id)) then
+ Set_Has_Partial_Visible_Refinement (State_Id);
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end;
+ end if;
+
-- Indicate that the private part is currently visible, so it can be
-- properly reset on exit.
-- On entrance to a package body, make declarations in package spec
-- immediately visible.
--
- -- When compiling the body of a package, both routines are called in
+ -- When compiling the body of a package, both routines are called in
-- succession. When compiling the body of a child package, the call
-- to Install_Private_Declaration is immediate for private children,
- -- but is deferred until the compilation of the private part of the
+ -- but is deferred until the compilation of the private part of the
-- child for public child packages.
function Unit_Requires_Body
Append_Elmt (Var_Id, Constits);
Set_Encapsulating_State (Var_Id, Encap_Id);
+
+ -- A Part_Of constituent partially refines an abstract state. This
+ -- property does not apply to protected or task units.
+
+ if Ekind (Encap_Id) = E_Abstract_State then
+ Set_Has_Partial_Visible_Refinement (Encap_Id);
+ end if;
end if;
-- Emit a clarification message when the encapsulator is undefined,
Add_Contract_Item (N, Item_Id);
- -- A variable may act as consituent of a single concurrent type
+ -- A variable may act as constituent of a single concurrent type
-- which in turn could be declared after the variable. Due to this
-- discrepancy, the full analysis of indicator Part_Of is delayed
-- until the end of the enclosing declarative region (see routine
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Posted : Boolean := False;
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Has_Missing : Boolean := False;
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
In_Seen : Boolean := False;
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Posted : Boolean := False;
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
- Refinement_Constituents (State_Id);
+ Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Proof_In_Seen : Boolean := False;
if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
and then Present (Encapsulating_State (Item_Id))
- and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
+ and then
+ (Has_Visible_Refinement (Encapsulating_State (Item_Id))
+ or else
+ Has_Partial_Visible_Refinement (Encapsulating_State (Item_Id)))
and then Contains (States, Encapsulating_State (Item_Id))
then
if Global_Mode = Name_Input then
-- Non-instance case
else
- -- The corresponding Global pragma must mention at least one state
- -- witha visible refinement at the point Refined_Global is processed.
- -- States with null refinements need Refined_Global pragma
- -- (SPARK RM 7.2.4(2)).
+ -- The corresponding Global pragma must mention at least one
+ -- state with a visible refinement at the point Refined_Global
+ -- is processed. States with null refinements need Refined_Global
+ -- pragma (SPARK RM 7.2.4(2)).
if not Has_In_State
and then not Has_In_Out_State