[multiple changes]
2014-02-04 Robert Dewar <dewar@adacore.com> * sinfo.ads: Further comments on N_Expression_With_Actions node. 2014-02-04 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Remove global variables Out_Items and Ref_Global. Remove local constant Body_Id along with dummy variables D1, D2, D3, D4, D5, D6, D7 and D8. Remove the useless collection of global items as this was a leftover from an earlier version of the routine. Move several routines out to avoid deep nesting and indentation. (Inputs_Match): Add formal parameter Dep_Clause. Rename formal parameter Do_Checks to Post_Errors. Update the comment on usage. (Is_Matching_Input): Renamed to Input_Match. Add formal parameters Ref_Inputs and Do_Checks. Rename formal parameter Do_Checks to Post_Errors. Update the comment on usage. Account for the case where a self referential state may have a null input_list. (Is_Self_Referential): New routine. 2014-02-04 Ed Schonberg <schonberg@adacore.com> * sem_ch13.adb (Analyze_Attribute_Definition_Clause): If the entity renames an expression, as in the case of an object of an unconstrained type initialized by a function call, defer the rewriting of the expression to the expander. * exp_ch13.adb (Expand_N_Attribute_Definition_Clause, case 'Alignment): If the entity renames an expression, introduce temporary to capture value, and rewrite original declaration to use temporary. From-SVN: r207467
This commit is contained in:
parent
ebdaa81b01
commit
81bd8c9075
@ -1,3 +1,34 @@
|
||||
2014-02-04 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* sinfo.ads: Further comments on N_Expression_With_Actions node.
|
||||
|
||||
2014-02-04 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Remove global
|
||||
variables Out_Items and Ref_Global. Remove local constant
|
||||
Body_Id along with dummy variables D1, D2, D3, D4, D5, D6, D7
|
||||
and D8. Remove the useless collection of global items as this
|
||||
was a leftover from an earlier version of the routine. Move
|
||||
several routines out to avoid deep nesting and indentation.
|
||||
(Inputs_Match): Add formal parameter Dep_Clause. Rename formal
|
||||
parameter Do_Checks to Post_Errors. Update the comment on usage.
|
||||
(Is_Matching_Input): Renamed to Input_Match. Add formal parameters
|
||||
Ref_Inputs and Do_Checks. Rename formal parameter Do_Checks
|
||||
to Post_Errors. Update the comment on usage. Account for the
|
||||
case where a self referential state may have a null input_list.
|
||||
(Is_Self_Referential): New routine.
|
||||
|
||||
2014-02-04 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_ch13.adb (Analyze_Attribute_Definition_Clause): If the
|
||||
entity renames an expression, as in the case of an object of
|
||||
an unconstrained type initialized by a function call, defer the
|
||||
rewriting of the expression to the expander.
|
||||
* exp_ch13.adb (Expand_N_Attribute_Definition_Clause, case
|
||||
'Alignment): If the entity renames an expression, introduce
|
||||
temporary to capture value, and rewrite original declaration to
|
||||
use temporary.
|
||||
|
||||
2014-02-04 Gary Dismukes <dismukes@adacore.com>
|
||||
|
||||
* g-comlin.adb: Minor typo fix.
|
||||
|
@ -157,6 +157,46 @@ package body Exp_Ch13 is
|
||||
(Exp, Make_Integer_Literal (Loc, Expr_Value (Exp)));
|
||||
end if;
|
||||
|
||||
-- A complex case arises if the alignment clause applies to an
|
||||
-- unconstrained object initialized with a function call. The
|
||||
-- result of the call is placed on the secondary stack, and the
|
||||
-- declaration is rewritten as a renaming of a dereference, which
|
||||
-- fails expansion. We must introduce a temporary and assign its
|
||||
-- value to the existing entity.
|
||||
|
||||
if Nkind (Parent (Ent)) = N_Object_Renaming_Declaration
|
||||
and then not Is_Entity_Name (Renamed_Object (Ent))
|
||||
then
|
||||
declare
|
||||
Loc : constant Source_Ptr := Sloc (N);
|
||||
Decl : constant Node_Id := Parent (Ent);
|
||||
Temp : constant Entity_Id := Make_Temporary (Loc, 'T');
|
||||
New_Decl : Node_Id;
|
||||
|
||||
begin
|
||||
-- Replace entity with temporary and renalyze
|
||||
|
||||
Set_Defining_Identifier (Decl, Temp);
|
||||
Set_Analyzed (Decl, False);
|
||||
Analyze (Decl);
|
||||
|
||||
-- Introduce new declaration for entity but do not reanalyze
|
||||
-- because entity is already in scope. Type and expression
|
||||
-- are already resolved.
|
||||
|
||||
New_Decl :=
|
||||
Make_Object_Declaration (Loc,
|
||||
Defining_Identifier => Ent,
|
||||
Object_Definition =>
|
||||
New_Occurrence_Of (Etype (Ent), Loc),
|
||||
Expression => New_Occurrence_Of (Temp, Loc));
|
||||
|
||||
Set_Renamed_Object (Ent, Empty);
|
||||
Insert_After (Decl, New_Decl);
|
||||
Set_Analyzed (Decl);
|
||||
end;
|
||||
end if;
|
||||
|
||||
------------------
|
||||
-- Storage_Size --
|
||||
------------------
|
||||
|
@ -3526,13 +3526,23 @@ package body Sem_Ch13 is
|
||||
-- expander. The easiest general way to handle this is to create a
|
||||
-- copy of the attribute definition clause for this object.
|
||||
|
||||
else
|
||||
elsif Is_Entity_Name (Renamed_Object (Ent)) then
|
||||
Insert_Action (N,
|
||||
Make_Attribute_Definition_Clause (Loc,
|
||||
Name =>
|
||||
New_Occurrence_Of (Entity (Renamed_Object (Ent)), Loc),
|
||||
Chars => Chars (N),
|
||||
Expression => Duplicate_Subexpr (Expression (N))));
|
||||
|
||||
-- If the renamed object is not an entity, it must be a dereference
|
||||
-- of an unconstrained function call, and we must introduce a new
|
||||
-- declaration to capture the expression. This is needed in the case
|
||||
-- of 'Alignment, where the original declaration must be rewritten.
|
||||
|
||||
else
|
||||
pragma Assert
|
||||
(Nkind (Renamed_Object (Ent)) = N_Explicit_Dereference);
|
||||
null;
|
||||
end if;
|
||||
|
||||
-- If no underlying entity, use entity itself, applies to some
|
||||
|
@ -21201,12 +21201,6 @@ package body Sem_Prag is
|
||||
Depends : Node_Id;
|
||||
-- The corresponding Depends pragma along with its clauses
|
||||
|
||||
Out_Items : Elist_Id := No_Elist;
|
||||
-- All output items as defined in pragma Refined_Global (if any)
|
||||
|
||||
Ref_Global : Node_Id := Empty;
|
||||
-- The corresponding Refined_Global pragma (if any)
|
||||
|
||||
Refinements : List_Id := No_List;
|
||||
-- The clauses of pragma Refined_Depends
|
||||
|
||||
@ -21216,6 +21210,27 @@ package body Sem_Prag is
|
||||
procedure Check_Dependency_Clause (Dep_Clause : Node_Id);
|
||||
-- Verify the legality of a single clause
|
||||
|
||||
function Input_Match
|
||||
(Dep_Input : Node_Id;
|
||||
Ref_Inputs : List_Id;
|
||||
Post_Errors : Boolean) return Boolean;
|
||||
-- Determine whether input Dep_Input matches one of inputs found in list
|
||||
-- Ref_Inputs. If flag Post_Errors is set, the routine reports missed or
|
||||
-- extra input items.
|
||||
|
||||
function Inputs_Match
|
||||
(Dep_Clause : Node_Id;
|
||||
Ref_Clause : Node_Id;
|
||||
Post_Errors : Boolean) return Boolean;
|
||||
-- Determine whether the inputs of Depends clause Dep_Clause match those
|
||||
-- of refinement clause Ref_Clause. If flag Post_Errors is set, then the
|
||||
-- routine reports missed or extra input items.
|
||||
|
||||
function Is_Self_Referential (Item_Id : Entity_Id) return Boolean;
|
||||
-- Determine whether a formal parameter, variable or state denoted by
|
||||
-- Item_Id appears both as input and an output in a single clause of
|
||||
-- pragma Depends.
|
||||
|
||||
procedure Report_Extra_Clauses;
|
||||
-- Emit an error for each extra clause the appears in Refined_Depends
|
||||
|
||||
@ -21224,327 +21239,6 @@ package body Sem_Prag is
|
||||
-----------------------------
|
||||
|
||||
procedure Check_Dependency_Clause (Dep_Clause : Node_Id) is
|
||||
function Inputs_Match
|
||||
(Ref_Clause : Node_Id;
|
||||
Do_Checks : Boolean) return Boolean;
|
||||
-- Determine whether the inputs of clause Dep_Clause match those of
|
||||
-- clause Ref_Clause. If flag Do_Checks is set, the routine reports
|
||||
-- missed or extra input items.
|
||||
|
||||
------------------
|
||||
-- Inputs_Match --
|
||||
------------------
|
||||
|
||||
function Inputs_Match
|
||||
(Ref_Clause : Node_Id;
|
||||
Do_Checks : Boolean) return Boolean
|
||||
is
|
||||
Ref_Inputs : List_Id;
|
||||
-- The input list of the refinement clause
|
||||
|
||||
function Is_Matching_Input (Dep_Input : Node_Id) return Boolean;
|
||||
-- Determine whether input Dep_Input matches one of the inputs of
|
||||
-- clause Ref_Clause.
|
||||
|
||||
procedure Report_Extra_Inputs;
|
||||
-- Emit errors for all extra inputs that appear in Ref_Clause
|
||||
|
||||
-----------------------
|
||||
-- Is_Matching_Input --
|
||||
-----------------------
|
||||
|
||||
function Is_Matching_Input (Dep_Input : Node_Id) return Boolean is
|
||||
procedure Match_Error (Msg : String; N : Node_Id);
|
||||
-- Emit a matching error if flag Do_Checks is set
|
||||
|
||||
-----------------
|
||||
-- Match_Error --
|
||||
-----------------
|
||||
|
||||
procedure Match_Error (Msg : String; N : Node_Id) is
|
||||
begin
|
||||
if Do_Checks then
|
||||
Error_Msg_N (Msg, N);
|
||||
end if;
|
||||
end Match_Error;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Dep_Id : Node_Id;
|
||||
Next_Ref_Input : Node_Id;
|
||||
Ref_Id : Entity_Id;
|
||||
Ref_Input : Node_Id;
|
||||
|
||||
Has_Constituent : Boolean := False;
|
||||
-- Flag set when the refinement input list contains at least
|
||||
-- one constituent of the state denoted by Dep_Id.
|
||||
|
||||
Has_Null_State : Boolean := False;
|
||||
-- Flag set when the dependency input is a state with a null
|
||||
-- refinement.
|
||||
|
||||
Has_Refined_State : Boolean := False;
|
||||
-- Flag set when the dependency input is a state with visible
|
||||
-- refinement.
|
||||
|
||||
-- Start of processing for Is_Matching_Input
|
||||
|
||||
begin
|
||||
-- Match a null input with another null input
|
||||
|
||||
if Nkind (Dep_Input) = N_Null then
|
||||
Ref_Input := First (Ref_Inputs);
|
||||
|
||||
-- Remove the matching null from the pool of candidates
|
||||
|
||||
if Nkind (Ref_Input) = N_Null then
|
||||
Remove (Ref_Input);
|
||||
return True;
|
||||
|
||||
else
|
||||
Match_Error
|
||||
("null input cannot be matched in corresponding "
|
||||
& "refinement clause", Dep_Input);
|
||||
end if;
|
||||
|
||||
-- Remaining cases are formal parameters, variables, and states
|
||||
|
||||
else
|
||||
-- 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.
|
||||
|
||||
Ref_Input := First (Ref_Inputs);
|
||||
while Present (Ref_Input) loop
|
||||
|
||||
-- Store the next input now because a match will remove
|
||||
-- it from the list.
|
||||
|
||||
Next_Ref_Input := Next (Ref_Input);
|
||||
|
||||
if Ekind (Dep_Id) = E_Abstract_State then
|
||||
|
||||
-- A state with a null refinement matches either a
|
||||
-- null input list or nothing at all (no input):
|
||||
|
||||
-- Refined_State => (State => null)
|
||||
|
||||
-- No input
|
||||
|
||||
-- Depends => (<output> => (State, Input))
|
||||
-- Refined_Depends => (<output> => Input) -- OK
|
||||
|
||||
-- Null input list
|
||||
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => null) -- OK
|
||||
|
||||
if Has_Null_Refinement (Dep_Id) then
|
||||
Has_Null_State := True;
|
||||
|
||||
-- Remove the matching null from the pool of
|
||||
-- candidates.
|
||||
|
||||
if Nkind (Ref_Input) = N_Null then
|
||||
Remove (Ref_Input);
|
||||
end if;
|
||||
|
||||
return True;
|
||||
|
||||
-- The state has a non-null refinement in which case
|
||||
-- remove all the matching constituents of the state:
|
||||
|
||||
-- Refined_State => (State => (C1, C2))
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => (C1, C2))
|
||||
|
||||
elsif Has_Non_Null_Refinement (Dep_Id) then
|
||||
Has_Refined_State := True;
|
||||
|
||||
-- Ref_Input is an entity name
|
||||
|
||||
if Is_Entity_Name (Ref_Input) then
|
||||
Ref_Id := Entity_Of (Ref_Input);
|
||||
|
||||
-- The input of the refinement clause is a valid
|
||||
-- constituent of the state. Remove the input
|
||||
-- from the pool of candidates. Note that the
|
||||
-- search continues because the state may be
|
||||
-- represented by multiple constituents.
|
||||
|
||||
if Ekind_In (Ref_Id, E_Abstract_State,
|
||||
E_Variable)
|
||||
and then Present (Encapsulating_State (Ref_Id))
|
||||
and then Encapsulating_State (Ref_Id) = Dep_Id
|
||||
then
|
||||
Has_Constituent := True;
|
||||
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
|
||||
-- entities. If this is the case, remove the input from
|
||||
-- the candidate list.
|
||||
|
||||
elsif Is_Entity_Name (Ref_Input)
|
||||
and then Entity_Of (Ref_Input) = Dep_Id
|
||||
then
|
||||
Remove (Ref_Input);
|
||||
return True;
|
||||
end if;
|
||||
|
||||
Ref_Input := Next_Ref_Input;
|
||||
end loop;
|
||||
|
||||
-- When a state with a null refinement appears as the last
|
||||
-- input, it matches nothing:
|
||||
|
||||
-- Refined_State => (State => null)
|
||||
-- Depends => (<output> => (Input, State))
|
||||
-- Refined_Depends => (<output> => Input) -- OK
|
||||
|
||||
if Ekind (Dep_Id) = E_Abstract_State
|
||||
and then Has_Null_Refinement (Dep_Id)
|
||||
and then No (Ref_Input)
|
||||
then
|
||||
Has_Null_State := True;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- A state with visible refinement was matched against one or
|
||||
-- more of its constituents.
|
||||
|
||||
if Has_Constituent then
|
||||
return True;
|
||||
|
||||
-- A state with a null refinement matched null or nothing
|
||||
|
||||
elsif Has_Null_State then
|
||||
return True;
|
||||
|
||||
-- The input of a dependence clause does not have a matching
|
||||
-- input in the refinement clause, emit an error.
|
||||
|
||||
else
|
||||
Match_Error
|
||||
("input cannot be matched in corresponding refinement "
|
||||
& "clause", Dep_Input);
|
||||
|
||||
if Has_Refined_State then
|
||||
Match_Error
|
||||
("\check the use of constituents in dependence "
|
||||
& "refinement", Dep_Input);
|
||||
end if;
|
||||
|
||||
return False;
|
||||
end if;
|
||||
end Is_Matching_Input;
|
||||
|
||||
-------------------------
|
||||
-- Report_Extra_Inputs --
|
||||
-------------------------
|
||||
|
||||
procedure Report_Extra_Inputs is
|
||||
Input : Node_Id;
|
||||
|
||||
begin
|
||||
if Present (Ref_Inputs) and then Do_Checks then
|
||||
Input := First (Ref_Inputs);
|
||||
while Present (Input) loop
|
||||
Error_Msg_N
|
||||
("unmatched or extra input in refinement clause",
|
||||
Input);
|
||||
|
||||
Next (Input);
|
||||
end loop;
|
||||
end if;
|
||||
end Report_Extra_Inputs;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Dep_Inputs : constant Node_Id := Expression (Dep_Clause);
|
||||
Inputs : constant Node_Id := Expression (Ref_Clause);
|
||||
Dep_Input : Node_Id;
|
||||
Result : Boolean;
|
||||
|
||||
-- Start of processing for Inputs_Match
|
||||
|
||||
begin
|
||||
-- Construct a list of all refinement inputs. Note that the input
|
||||
-- list is copied because the algorithm modifies its contents and
|
||||
-- this should not be visible in Refined_Depends.
|
||||
|
||||
if Nkind (Inputs) = N_Aggregate then
|
||||
Ref_Inputs := New_Copy_List (Expressions (Inputs));
|
||||
else
|
||||
Ref_Inputs := New_List (Inputs);
|
||||
end if;
|
||||
|
||||
-- Depending on whether the original dependency clause mentions
|
||||
-- states with visible refinement, the corresponding refinement
|
||||
-- clause may differ greatly in structure and contents:
|
||||
|
||||
-- State with null refinement
|
||||
|
||||
-- Refined_State => (State => null)
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => null)
|
||||
|
||||
-- Depends => (<output> => (State, Input))
|
||||
-- Refined_Depends => (<output> => Input)
|
||||
|
||||
-- Depends => (<output> => (Input_1, State, Input_2))
|
||||
-- Refined_Depends => (<output> => (Input_1, Input_2))
|
||||
|
||||
-- State with non-null refinement
|
||||
|
||||
-- Refined_State => (State_1 => (C1, C2))
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => C1)
|
||||
-- or
|
||||
-- Refined_Depends => (<output> => (C1, C2))
|
||||
|
||||
if Nkind (Dep_Inputs) = N_Aggregate then
|
||||
Dep_Input := First (Expressions (Dep_Inputs));
|
||||
while Present (Dep_Input) loop
|
||||
if not Is_Matching_Input (Dep_Input) then
|
||||
Result := False;
|
||||
end if;
|
||||
|
||||
Next (Dep_Input);
|
||||
end loop;
|
||||
|
||||
Result := True;
|
||||
|
||||
-- Solitary input
|
||||
|
||||
else
|
||||
Result := Is_Matching_Input (Dep_Inputs);
|
||||
end if;
|
||||
|
||||
Report_Extra_Inputs;
|
||||
return Result;
|
||||
end Inputs_Match;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Dep_Output : constant Node_Id := First (Choices (Dep_Clause));
|
||||
Dep_Id : Entity_Id;
|
||||
Matching_Clause : Node_Id := Empty;
|
||||
@ -21565,8 +21259,6 @@ package body Sem_Prag is
|
||||
-- Flag set when the output of clause Dep_Clause is a state with
|
||||
-- visible refinement.
|
||||
|
||||
-- Start of processing for Check_Dependency_Clause
|
||||
|
||||
begin
|
||||
-- The analysis of pragma Depends should produce normalized clauses
|
||||
-- with exactly one output. This is important because output items
|
||||
@ -21681,7 +21373,9 @@ package body Sem_Prag is
|
||||
and then Present (Encapsulating_State (Ref_Id))
|
||||
and then Encapsulating_State (Ref_Id) = Dep_Id
|
||||
and then Inputs_Match
|
||||
(Ref_Clause, Do_Checks => False)
|
||||
(Dep_Clause => Dep_Clause,
|
||||
Ref_Clause => Ref_Clause,
|
||||
Post_Errors => False)
|
||||
then
|
||||
Has_Constituent := True;
|
||||
Remove (Ref_Clause);
|
||||
@ -21742,7 +21436,11 @@ package body Sem_Prag is
|
||||
-- from the pool of candidates.
|
||||
|
||||
if Present (Matching_Clause) then
|
||||
if Inputs_Match (Matching_Clause, Do_Checks => True) then
|
||||
if Inputs_Match
|
||||
(Ref_Clause => Ref_Clause,
|
||||
Dep_Clause => Matching_Clause,
|
||||
Post_Errors => True)
|
||||
then
|
||||
Remove (Matching_Clause);
|
||||
end if;
|
||||
|
||||
@ -21773,6 +21471,415 @@ package body Sem_Prag is
|
||||
end if;
|
||||
end Check_Dependency_Clause;
|
||||
|
||||
-----------------
|
||||
-- Input_Match --
|
||||
-----------------
|
||||
|
||||
function Input_Match
|
||||
(Dep_Input : Node_Id;
|
||||
Ref_Inputs : List_Id;
|
||||
Post_Errors : Boolean) return Boolean
|
||||
is
|
||||
procedure Match_Error (Msg : String; N : Node_Id);
|
||||
-- Emit a matching error if flag Post_Errors is set
|
||||
|
||||
-----------------
|
||||
-- Match_Error --
|
||||
-----------------
|
||||
|
||||
procedure Match_Error (Msg : String; N : Node_Id) is
|
||||
begin
|
||||
if Post_Errors then
|
||||
Error_Msg_N (Msg, N);
|
||||
end if;
|
||||
end Match_Error;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Dep_Id : Node_Id;
|
||||
Next_Ref_Input : Node_Id;
|
||||
Ref_Id : Entity_Id;
|
||||
Ref_Input : Node_Id;
|
||||
|
||||
Has_Constituent : Boolean := False;
|
||||
-- Flag set when the refinement input list contains at least one
|
||||
-- constituent of the state denoted by Dep_Id.
|
||||
|
||||
Has_Null_State : Boolean := False;
|
||||
-- Flag set when the dependency input is a state with a visible null
|
||||
-- refinement.
|
||||
|
||||
Has_Refined_State : Boolean := False;
|
||||
-- Flag set when the dependency input is a state with visible non-
|
||||
-- null refinement.
|
||||
|
||||
-- Start of processing for Input_Match
|
||||
|
||||
begin
|
||||
-- Match a null input with another null input
|
||||
|
||||
if Nkind (Dep_Input) = N_Null then
|
||||
Ref_Input := First (Ref_Inputs);
|
||||
|
||||
-- Remove the matching null from the pool of candidates
|
||||
|
||||
if Nkind (Ref_Input) = N_Null then
|
||||
Remove (Ref_Input);
|
||||
return True;
|
||||
|
||||
else
|
||||
Match_Error
|
||||
("null input cannot be matched in corresponding refinement "
|
||||
& "clause", Dep_Input);
|
||||
end if;
|
||||
|
||||
-- Remaining cases are formal parameters, variables, and states
|
||||
|
||||
else
|
||||
-- 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.
|
||||
|
||||
Ref_Input := First (Ref_Inputs);
|
||||
while Present (Ref_Input) loop
|
||||
|
||||
-- Store the next input now because a match will remove it from
|
||||
-- the list.
|
||||
|
||||
Next_Ref_Input := Next (Ref_Input);
|
||||
|
||||
if Ekind (Dep_Id) = E_Abstract_State then
|
||||
|
||||
-- A state with a null refinement matches either a null
|
||||
-- input list or nothing at all (no input):
|
||||
|
||||
-- Refined_State => (State => null)
|
||||
|
||||
-- No input
|
||||
|
||||
-- Depends => (<output> => (State, Input))
|
||||
-- Refined_Depends => (<output> => Input) -- OK
|
||||
|
||||
-- Null input list
|
||||
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => null) -- OK
|
||||
|
||||
if Has_Null_Refinement (Dep_Id) then
|
||||
Has_Null_State := True;
|
||||
|
||||
-- Remove the matching null from the pool of candidates
|
||||
|
||||
if Nkind (Ref_Input) = N_Null then
|
||||
Remove (Ref_Input);
|
||||
end if;
|
||||
|
||||
return True;
|
||||
|
||||
-- The state has a non-null refinement in which case remove
|
||||
-- all the matching constituents of the state:
|
||||
|
||||
-- Refined_State => (State => (C1, C2))
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => (C1, C2))
|
||||
|
||||
elsif Has_Non_Null_Refinement (Dep_Id) then
|
||||
Has_Refined_State := True;
|
||||
|
||||
-- A state with a visible non-null refinement may have a
|
||||
-- null input_list only when it is self referential.
|
||||
|
||||
-- Refined_State => (State => (C1, C2))
|
||||
-- Depends => (State => State)
|
||||
-- Refined_Depends => (C2 => null) -- OK
|
||||
|
||||
if Nkind (Ref_Input) = N_Null
|
||||
and then Is_Self_Referential (Dep_Id)
|
||||
then
|
||||
-- Remove the null from the pool of candidates. Note
|
||||
-- that the search continues because the state may be
|
||||
-- represented by multiple constituents.
|
||||
|
||||
Has_Constituent := True;
|
||||
Remove (Ref_Input);
|
||||
|
||||
-- Ref_Input is an entity name
|
||||
|
||||
elsif Is_Entity_Name (Ref_Input) then
|
||||
Ref_Id := Entity_Of (Ref_Input);
|
||||
|
||||
-- The input of the refinement clause is a valid
|
||||
-- constituent of the state. Remove the input from the
|
||||
-- pool of candidates. Note that the search continues
|
||||
-- because the state may be represented by multiple
|
||||
-- constituents.
|
||||
|
||||
if Ekind_In (Ref_Id, E_Abstract_State,
|
||||
E_Variable)
|
||||
and then Present (Encapsulating_State (Ref_Id))
|
||||
and then Encapsulating_State (Ref_Id) = Dep_Id
|
||||
then
|
||||
Has_Constituent := True;
|
||||
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 entities. If
|
||||
-- this is the case, remove the input from the candidate list.
|
||||
|
||||
elsif Is_Entity_Name (Ref_Input)
|
||||
and then Entity_Of (Ref_Input) = Dep_Id
|
||||
then
|
||||
Remove (Ref_Input);
|
||||
return True;
|
||||
end if;
|
||||
|
||||
Ref_Input := Next_Ref_Input;
|
||||
end loop;
|
||||
|
||||
-- When a state with a null refinement appears as the last input,
|
||||
-- it matches nothing:
|
||||
|
||||
-- Refined_State => (State => null)
|
||||
-- Depends => (<output> => (Input, State))
|
||||
-- Refined_Depends => (<output> => Input) -- OK
|
||||
|
||||
if Ekind (Dep_Id) = E_Abstract_State
|
||||
and then Has_Null_Refinement (Dep_Id)
|
||||
and then No (Ref_Input)
|
||||
then
|
||||
Has_Null_State := True;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- A state with visible refinement was matched against one or more of
|
||||
-- its constituents.
|
||||
|
||||
if Has_Constituent then
|
||||
return True;
|
||||
|
||||
-- A state with a null refinement matched null or nothing
|
||||
|
||||
elsif Has_Null_State then
|
||||
return True;
|
||||
|
||||
-- The input of a dependence clause does not have a matching input in
|
||||
-- the refinement clause, emit an error.
|
||||
|
||||
else
|
||||
Match_Error
|
||||
("input cannot be matched in corresponding refinement clause",
|
||||
Dep_Input);
|
||||
|
||||
if Has_Refined_State then
|
||||
Match_Error
|
||||
("\check the use of constituents in dependence refinement",
|
||||
Dep_Input);
|
||||
end if;
|
||||
|
||||
return False;
|
||||
end if;
|
||||
end Input_Match;
|
||||
|
||||
------------------
|
||||
-- Inputs_Match --
|
||||
------------------
|
||||
|
||||
function Inputs_Match
|
||||
(Dep_Clause : Node_Id;
|
||||
Ref_Clause : Node_Id;
|
||||
Post_Errors : Boolean) return Boolean
|
||||
is
|
||||
Ref_Inputs : List_Id;
|
||||
-- The input list of the refinement clause
|
||||
|
||||
procedure Report_Extra_Inputs;
|
||||
-- Emit errors for all extra inputs that appear in Ref_Inputs
|
||||
|
||||
-------------------------
|
||||
-- Report_Extra_Inputs --
|
||||
-------------------------
|
||||
|
||||
procedure Report_Extra_Inputs is
|
||||
Input : Node_Id;
|
||||
|
||||
begin
|
||||
if Present (Ref_Inputs) and then Post_Errors then
|
||||
Input := First (Ref_Inputs);
|
||||
while Present (Input) loop
|
||||
Error_Msg_N
|
||||
("unmatched or extra input in refinement clause", Input);
|
||||
|
||||
Next (Input);
|
||||
end loop;
|
||||
end if;
|
||||
end Report_Extra_Inputs;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Dep_Inputs : constant Node_Id := Expression (Dep_Clause);
|
||||
Inputs : constant Node_Id := Expression (Ref_Clause);
|
||||
Dep_Input : Node_Id;
|
||||
Result : Boolean;
|
||||
|
||||
-- Start of processing for Inputs_Match
|
||||
|
||||
begin
|
||||
-- Construct a list of all refinement inputs. Note that the input
|
||||
-- list is copied because the algorithm modifies its contents and
|
||||
-- this should not be visible in Refined_Depends.
|
||||
|
||||
if Nkind (Inputs) = N_Aggregate then
|
||||
Ref_Inputs := New_Copy_List (Expressions (Inputs));
|
||||
else
|
||||
Ref_Inputs := New_List (Inputs);
|
||||
end if;
|
||||
|
||||
-- Depending on whether the original dependency clause mentions
|
||||
-- states with visible refinement, the corresponding refinement
|
||||
-- clause may differ greatly in structure and contents:
|
||||
|
||||
-- State with null refinement
|
||||
|
||||
-- Refined_State => (State => null)
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => null)
|
||||
|
||||
-- Depends => (<output> => (State, Input))
|
||||
-- Refined_Depends => (<output> => Input)
|
||||
|
||||
-- Depends => (<output> => (Input_1, State, Input_2))
|
||||
-- Refined_Depends => (<output> => (Input_1, Input_2))
|
||||
|
||||
-- State with non-null refinement
|
||||
|
||||
-- Refined_State => (State_1 => (C1, C2))
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => C1)
|
||||
-- or
|
||||
-- Refined_Depends => (<output> => (C1, C2))
|
||||
|
||||
if Nkind (Dep_Inputs) = N_Aggregate then
|
||||
Dep_Input := First (Expressions (Dep_Inputs));
|
||||
while Present (Dep_Input) loop
|
||||
if not Input_Match
|
||||
(Dep_Input => Dep_Input,
|
||||
Ref_Inputs => Ref_Inputs,
|
||||
Post_Errors => Post_Errors)
|
||||
then
|
||||
Result := False;
|
||||
end if;
|
||||
|
||||
Next (Dep_Input);
|
||||
end loop;
|
||||
|
||||
Result := True;
|
||||
|
||||
-- Solitary input
|
||||
|
||||
else
|
||||
Result :=
|
||||
Input_Match
|
||||
(Dep_Input => Dep_Inputs,
|
||||
Ref_Inputs => Ref_Inputs,
|
||||
Post_Errors => Post_Errors);
|
||||
end if;
|
||||
|
||||
-- List all inputs that appear as extras
|
||||
|
||||
Report_Extra_Inputs;
|
||||
|
||||
return Result;
|
||||
end Inputs_Match;
|
||||
|
||||
-------------------------
|
||||
-- Is_Self_Referential --
|
||||
-------------------------
|
||||
|
||||
function Is_Self_Referential (Item_Id : Entity_Id) return Boolean is
|
||||
function Denotes_Item (N : Node_Id) return Boolean;
|
||||
-- Determine whether an arbitrary node N denotes item Item_Id
|
||||
|
||||
------------------
|
||||
-- Denotes_Item --
|
||||
------------------
|
||||
|
||||
function Denotes_Item (N : Node_Id) return Boolean is
|
||||
begin
|
||||
return
|
||||
Is_Entity_Name (N)
|
||||
and then Present (Entity (N))
|
||||
and then Entity (N) = Item_Id;
|
||||
end Denotes_Item;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Clauses : constant Node_Id :=
|
||||
Get_Pragma_Arg
|
||||
(First (Pragma_Argument_Associations (Depends)));
|
||||
Clause : Node_Id;
|
||||
Input : Node_Id;
|
||||
Output : Node_Id;
|
||||
|
||||
-- Start of processing for Is_Self_Referential
|
||||
|
||||
begin
|
||||
Clause := First (Component_Associations (Clauses));
|
||||
while Present (Clause) loop
|
||||
|
||||
-- Due to normalization, a dependence clause has exactly one
|
||||
-- output even if the original clause had multiple outputs.
|
||||
|
||||
Output := First (Choices (Clause));
|
||||
|
||||
-- Detect the following scenario:
|
||||
--
|
||||
-- Item_Id => [(...,] Item_Id [, ...)]
|
||||
|
||||
if Denotes_Item (Output) then
|
||||
Input := Expression (Clause);
|
||||
|
||||
-- Multiple inputs appear as an aggregate
|
||||
|
||||
if Nkind (Input) = N_Aggregate then
|
||||
Input := First (Expressions (Input));
|
||||
|
||||
if Denotes_Item (Input) then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
Next (Input);
|
||||
|
||||
-- Solitary input
|
||||
|
||||
elsif Denotes_Item (Input) then
|
||||
return True;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next (Clause);
|
||||
end loop;
|
||||
|
||||
return False;
|
||||
end Is_Self_Referential;
|
||||
|
||||
--------------------------
|
||||
-- Report_Extra_Clauses --
|
||||
--------------------------
|
||||
@ -21804,18 +21911,11 @@ package body Sem_Prag is
|
||||
-- Local variables
|
||||
|
||||
Body_Decl : constant Node_Id := Parent (N);
|
||||
Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
|
||||
Errors : constant Nat := Serious_Errors_Detected;
|
||||
Clause : Node_Id;
|
||||
Deps : Node_Id;
|
||||
Refs : Node_Id;
|
||||
|
||||
-- The following are dummy variables that capture unused output of
|
||||
-- routine Collect_Global_Items.
|
||||
|
||||
D1, D2, D3 : Elist_Id := No_Elist;
|
||||
D4, D5, D6, D7, D8 : Boolean;
|
||||
|
||||
-- Start of processing for Analyze_Refined_Depends_In_Decl_Part
|
||||
|
||||
begin
|
||||
@ -21859,28 +21959,6 @@ package body Sem_Prag is
|
||||
Refs := Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
|
||||
|
||||
if Serious_Errors_Detected = Errors then
|
||||
|
||||
-- The related subprogram may be subject to pragma Refined_Global. If
|
||||
-- this is the case, gather all output items. These are needed when
|
||||
-- verifying the use of constituents that apply to output states with
|
||||
-- visible refinement.
|
||||
|
||||
Ref_Global := Get_Pragma (Body_Id, Pragma_Refined_Global);
|
||||
|
||||
if Present (Ref_Global) then
|
||||
Collect_Global_Items
|
||||
(Prag => Ref_Global,
|
||||
In_Items => D1,
|
||||
In_Out_Items => D2,
|
||||
Out_Items => Out_Items,
|
||||
Proof_In_Items => D3,
|
||||
Has_In_State => D4,
|
||||
Has_In_Out_State => D5,
|
||||
Has_Out_State => D6,
|
||||
Has_Proof_In_State => D7,
|
||||
Has_Null_State => D8);
|
||||
end if;
|
||||
|
||||
if Nkind (Refs) = N_Null then
|
||||
Refinements := No_List;
|
||||
|
||||
|
@ -7359,7 +7359,11 @@ package Sinfo is
|
||||
-- the actions list is always non-null, since there is no point in this
|
||||
-- node if the actions are Empty. During semantic analysis there are
|
||||
-- cases where it is convenient to temporarily generate an empty actions
|
||||
-- list, but the Expander removes such cases.
|
||||
-- list. This arises in cases where we create such an empty actions
|
||||
-- list, and it may or may not end up being a place where additional
|
||||
-- actions are inserted. The expander removes such empty cases after
|
||||
-- the expression of the node is fully analyzed and expanded, at which
|
||||
-- point it is safe to remove it, since no more actions can be inserted.
|
||||
|
||||
-- Note: Expression may be a Null_Statement, in which case the
|
||||
-- N_Expression_With_Actions has type Standard_Void_Type. However some
|
||||
|
Loading…
Reference in New Issue
Block a user