[multiple changes]
2014-11-20 Ed Schonberg <schonberg@adacore.com> * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Do not apply inlining expansion if function build in place, i.e. has a limited return type. 2014-11-20 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Add variables Body_Id, Body_Inputs, Body_Outputs, Spec_Inputs, Spec_Outputs. Synthesize the inputs and outputs of the subprogram when pragma [Refined_]Global is missing and perform legality checks on output states with visible refinement. (Appears_In): Update the comment on usage. (Check_Output_States): New routine. (Collect_Dependency_Clause): New routine. (Collect_Global_Items): Relocated to Analyze_Refined_Global_In_Decl_Part. (Collect_Subprogram_Inputs_Outputs): Add new formal parameters Synthesize and Depends_Seen. The routine can now synthesize inputs and outputs from pragma [Refined_]Depends. (Normalize_Clause): Update the comment on usage. The routine no longer performs normalization of outputs. (Normalize_Clauses): Normalize both inputs and outputs. (Normalize_Output): Relocated to Normalize_Clauses. * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Add new formal parameters Synthesize and Depends_Seen and update the comment on usage. 2014-11-20 Ed Schonberg <schonberg@adacore.com> * sem_ch13.adb (Reset_Loop_Variable): New subsidiary procedure in Build_Predicate_Functions, to handle properly quantified expressions in dynamic predicates. From-SVN: r217850
This commit is contained in:
parent
bfe25016e3
commit
5c5e108f9b
|
@ -1,3 +1,44 @@
|
|||
2014-11-20 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Do not apply
|
||||
inlining expansion if function build in place, i.e. has a limited
|
||||
return type.
|
||||
|
||||
2014-11-20 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Add
|
||||
variables Body_Id, Body_Inputs, Body_Outputs, Spec_Inputs,
|
||||
Spec_Outputs. Synthesize the inputs and outputs of the subprogram
|
||||
when pragma [Refined_]Global is missing and perform legality
|
||||
checks on output states with visible refinement.
|
||||
(Appears_In): Update the comment on usage.
|
||||
(Check_Output_States): New routine.
|
||||
(Collect_Dependency_Clause): New routine.
|
||||
(Collect_Global_Items): Relocated to
|
||||
Analyze_Refined_Global_In_Decl_Part.
|
||||
(Collect_Subprogram_Inputs_Outputs): Add new formal parameters
|
||||
Synthesize and Depends_Seen. The routine can now synthesize inputs
|
||||
and outputs from pragma [Refined_]Depends.
|
||||
(Normalize_Clause): Update the comment on usage. The routine no longer
|
||||
performs normalization of outputs.
|
||||
(Normalize_Clauses): Normalize both inputs and outputs.
|
||||
(Normalize_Output): Relocated to Normalize_Clauses.
|
||||
* sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Add new
|
||||
formal parameters Synthesize and Depends_Seen and update the
|
||||
comment on usage.
|
||||
|
||||
2014-11-20 Vincent Celier <celier@adacore.com>
|
||||
|
||||
PR ada/47500
|
||||
* back_end.adb (Scan_Back_End_Switches): Skip switch -G and
|
||||
its argument.
|
||||
|
||||
2014-11-20 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_ch13.adb (Reset_Loop_Variable): New subsidiary procedure
|
||||
in Build_Predicate_Functions, to handle properly quantified
|
||||
expressions in dynamic predicates.
|
||||
|
||||
2014-11-20 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* gnatcmd.adb, sem_ch6.adb, exp_dist.adb: Minor reformatting.
|
||||
|
|
|
@ -2853,6 +2853,7 @@ package body Sem_Ch13 is
|
|||
begin
|
||||
if A_Id = Aspect_Pre or else A_Id = Aspect_Precondition then
|
||||
Pname := Name_Precondition;
|
||||
|
||||
else
|
||||
Pname := Name_Postcondition;
|
||||
end if;
|
||||
|
@ -2925,6 +2926,7 @@ package body Sem_Ch13 is
|
|||
-- with delay of visibility for the expression analysis.
|
||||
|
||||
Insert_Pragma (Aitem);
|
||||
|
||||
goto Continue;
|
||||
end Pre_Post;
|
||||
|
||||
|
@ -3552,7 +3554,7 @@ package body Sem_Ch13 is
|
|||
-- the type of the formal match.
|
||||
|
||||
if Base_Type (Typ) /= Base_Type (Ent)
|
||||
or else Present ((Next_Formal (F)))
|
||||
or else Present (Next_Formal (F))
|
||||
then
|
||||
return False;
|
||||
|
||||
|
@ -3630,7 +3632,8 @@ package body Sem_Ch13 is
|
|||
Error_Msg_N ("stream subprogram must not be abstract", Expr);
|
||||
return;
|
||||
|
||||
-- Test for stream subprogram for interface type being non-null
|
||||
-- A stream subprogram for an interface type must be a null
|
||||
-- procedure (RM 13.13.2 (38/3)).
|
||||
|
||||
elsif Is_Interface (U_Ent)
|
||||
and then not Inside_A_Generic
|
||||
|
@ -8268,11 +8271,44 @@ package body Sem_Ch13 is
|
|||
|
||||
if Raise_Expression_Present then
|
||||
declare
|
||||
Map : constant Elist_Id := New_Elmt_List;
|
||||
Map : constant Elist_Id := New_Elmt_List;
|
||||
New_V : Entity_Id := Empty;
|
||||
|
||||
-- The unanalyzed expression will be copied and appear in
|
||||
-- both functions. Normally expressions do not declare new
|
||||
-- entities, but quantified expressions do, so we need to
|
||||
-- create new entities for their bound variables, to prevent
|
||||
-- multiple definitions in gigi.
|
||||
|
||||
function Reset_Loop_Variable (N : Node_Id)
|
||||
return Traverse_Result;
|
||||
|
||||
procedure Collect_Loop_Variables is
|
||||
new Traverse_Proc (Reset_Loop_Variable);
|
||||
|
||||
------------------------
|
||||
-- Reset_Loop_Variable --
|
||||
------------------------
|
||||
|
||||
function Reset_Loop_Variable (N : Node_Id)
|
||||
return Traverse_Result
|
||||
is
|
||||
begin
|
||||
if Nkind (N) = N_Iterator_Specification then
|
||||
New_V := Make_Defining_Identifier
|
||||
(Sloc (N), Chars (Defining_Identifier (N)));
|
||||
|
||||
Set_Defining_Identifier (N, New_V);
|
||||
end if;
|
||||
|
||||
return OK;
|
||||
end Reset_Loop_Variable;
|
||||
|
||||
begin
|
||||
Append_Elmt (Object_Entity, Map);
|
||||
Append_Elmt (Object_Entity_M, Map);
|
||||
Expr_M := New_Copy_Tree (Expr, Map => Map);
|
||||
Collect_Loop_Variables (Expr_M);
|
||||
end;
|
||||
end if;
|
||||
|
||||
|
|
|
@ -3691,6 +3691,11 @@ package body Sem_Ch6 is
|
|||
if Comes_From_Source (Body_Id)
|
||||
and then Ekind (Spec_Id) = E_Function
|
||||
and then Returns_Unconstrained_Type (Spec_Id)
|
||||
|
||||
-- If function builds in place, i.e. returns a limited type,
|
||||
-- inlining cannot be done.
|
||||
|
||||
and then not Is_Limited_Type (Etype (Spec_Id))
|
||||
then
|
||||
Check_And_Split_Unconstrained_Function (N, Spec_Id, Body_Id);
|
||||
|
||||
|
|
|
@ -178,9 +178,9 @@ package body Sem_Prag is
|
|||
-- casing is constructed.
|
||||
|
||||
function Appears_In (List : Elist_Id; Item_Id : Entity_Id) return Boolean;
|
||||
-- Subsidiary to the analysis of pragma Global and pragma Depends. Query
|
||||
-- whether a particular item appears in a mixed list of nodes and entities.
|
||||
-- It is assumed that all nodes in the list have entities.
|
||||
-- Subsidiary to analysis of pragmas Depends, Global and Refined_Depends.
|
||||
-- Query whether a particular item appears in a mixed list of nodes and
|
||||
-- entities. It is assumed that all nodes in the list have entities.
|
||||
|
||||
function Check_Kind (Nam : Name_Id) return Name_Id;
|
||||
-- This function is used in connection with pragmas Assert, Check,
|
||||
|
@ -216,25 +216,6 @@ package body Sem_Prag is
|
|||
-- corresponding constituent from list Constits (if any) appear in the same
|
||||
-- context denoted by Context. If this is the case, emit an error.
|
||||
|
||||
procedure Collect_Global_Items
|
||||
(Prag : Node_Id;
|
||||
In_Items : in out Elist_Id;
|
||||
In_Out_Items : in out Elist_Id;
|
||||
Out_Items : in out Elist_Id;
|
||||
Proof_In_Items : in out Elist_Id;
|
||||
Has_In_State : out Boolean;
|
||||
Has_In_Out_State : out Boolean;
|
||||
Has_Out_State : out Boolean;
|
||||
Has_Proof_In_State : out Boolean;
|
||||
Has_Null_State : out Boolean);
|
||||
-- Subsidiary to the analysis of pragma Refined_Depends/Refined_Global.
|
||||
-- Prag denotes pragma [Refined_]Global. Gather all input, in out, output
|
||||
-- and Proof_In items of Prag in lists In_Items, In_Out_Items, Out_Items
|
||||
-- and Proof_In_Items. Flags Has_In_State, Has_In_Out_State, Has_Out_State
|
||||
-- and Has_Proof_In_State are set when there is at least one abstract state
|
||||
-- with visible refinement available in the corresponding mode. Flag
|
||||
-- Has_Null_State is set when at least state has a null refinement.
|
||||
|
||||
function Find_Related_Subprogram_Or_Body
|
||||
(Prag : Node_Id;
|
||||
Do_Checks : Boolean := False) return Node_Id;
|
||||
|
@ -581,9 +562,7 @@ package body Sem_Prag is
|
|||
-- error if this is not the case.
|
||||
|
||||
procedure Normalize_Clause (Clause : Node_Id);
|
||||
-- Remove a self-dependency "+" from the input list of a clause. Split
|
||||
-- a clause with multiple outputs into multiple clauses with a single
|
||||
-- output.
|
||||
-- Remove a self-dependency "+" from the input list of a clause
|
||||
|
||||
-----------------------------
|
||||
-- Add_Item_To_Name_Buffer --
|
||||
|
@ -1335,11 +1314,6 @@ package body Sem_Prag is
|
|||
-- Flag Multiple should be set when Output comes from a list with
|
||||
-- multiple items.
|
||||
|
||||
procedure Normalize_Outputs;
|
||||
-- If Clause contains more than one output, split the clause into
|
||||
-- multiple clauses with a single output. All new clauses are added
|
||||
-- after Clause.
|
||||
|
||||
-----------------------------
|
||||
-- Create_Or_Modify_Clause --
|
||||
-----------------------------
|
||||
|
@ -1525,68 +1499,6 @@ package body Sem_Prag is
|
|||
end if;
|
||||
end Create_Or_Modify_Clause;
|
||||
|
||||
-----------------------
|
||||
-- Normalize_Outputs --
|
||||
-----------------------
|
||||
|
||||
procedure Normalize_Outputs is
|
||||
Inputs : constant Node_Id := Expression (Clause);
|
||||
Loc : constant Source_Ptr := Sloc (Clause);
|
||||
Outputs : constant Node_Id := First (Choices (Clause));
|
||||
Last_Output : Node_Id;
|
||||
New_Clause : Node_Id;
|
||||
Next_Output : Node_Id;
|
||||
Output : Node_Id;
|
||||
|
||||
begin
|
||||
-- Multiple outputs appear as an aggregate. Nothing to do when
|
||||
-- the clause has exactly one output.
|
||||
|
||||
if Nkind (Outputs) = N_Aggregate then
|
||||
Last_Output := Last (Expressions (Outputs));
|
||||
|
||||
-- Create a clause for each output. Note that each time a new
|
||||
-- clause is created, the original output list slowly shrinks
|
||||
-- until there is one item left.
|
||||
|
||||
Output := First (Expressions (Outputs));
|
||||
while Present (Output) loop
|
||||
Next_Output := Next (Output);
|
||||
|
||||
-- Unhook the output from the original output list as it
|
||||
-- will be relocated to a new clause.
|
||||
|
||||
Remove (Output);
|
||||
|
||||
-- Special processing for the last output. At this point
|
||||
-- the original aggregate has been stripped down to one
|
||||
-- element. Replace the aggregate by the element itself.
|
||||
|
||||
if Output = Last_Output then
|
||||
Rewrite (Outputs, Output);
|
||||
|
||||
else
|
||||
-- Generate a clause of the form:
|
||||
-- (Output => Inputs)
|
||||
|
||||
New_Clause :=
|
||||
Make_Component_Association (Loc,
|
||||
Choices => New_List (Output),
|
||||
Expression => New_Copy_Tree (Inputs));
|
||||
|
||||
-- The new clause contains replicated content that has
|
||||
-- already been analyzed. There is not need to reanalyze
|
||||
-- them.
|
||||
|
||||
Set_Analyzed (New_Clause);
|
||||
Insert_After (Clause, New_Clause);
|
||||
end if;
|
||||
|
||||
Output := Next_Output;
|
||||
end loop;
|
||||
end if;
|
||||
end Normalize_Outputs;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Outputs : constant Node_Id := First (Choices (Clause));
|
||||
|
@ -1641,11 +1553,6 @@ package body Sem_Prag is
|
|||
Multiple => False);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Split a clause with multiple outputs into multiple clauses with a
|
||||
-- single output.
|
||||
|
||||
Normalize_Outputs;
|
||||
end Normalize_Clause;
|
||||
|
||||
-- Local variables
|
||||
|
@ -21856,6 +21763,11 @@ package body Sem_Prag is
|
|||
------------------------------------------
|
||||
|
||||
procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id) is
|
||||
Body_Inputs : Elist_Id := No_Elist;
|
||||
Body_Outputs : Elist_Id := No_Elist;
|
||||
-- The inputs and outputs of the subprogram body synthesized from pragma
|
||||
-- Refined_Depends.
|
||||
|
||||
Dependencies : List_Id := No_List;
|
||||
Depends : Node_Id;
|
||||
-- The corresponding Depends pragma along with its clauses
|
||||
|
@ -21870,11 +21782,21 @@ package body Sem_Prag is
|
|||
Spec_Id : Entity_Id;
|
||||
-- The entity of the subprogram subject to pragma Refined_Depends
|
||||
|
||||
Spec_Inputs : Elist_Id := No_Elist;
|
||||
Spec_Outputs : Elist_Id := No_Elist;
|
||||
-- The inputs and outputs of the subprogram spec synthesized from pragma
|
||||
-- Depends.
|
||||
|
||||
procedure Check_Dependency_Clause (Dep_Clause : Node_Id);
|
||||
-- Try to match a single dependency clause Dep_Clause against one or
|
||||
-- more refinement clauses found in list Refinements. Each successful
|
||||
-- match eliminates at least one refinement clause from Refinements.
|
||||
|
||||
procedure Check_Output_States;
|
||||
-- Determine whether pragma Depends contains an output state with a
|
||||
-- visible refinement and if so, ensure that pragma Refined_Depends
|
||||
-- mentions all its constituents as outputs.
|
||||
|
||||
procedure Normalize_Clauses (Clauses : List_Id);
|
||||
-- Given a list of dependence or refinement clauses Clauses, normalize
|
||||
-- each clause by creating multiple dependencies with exactly one input
|
||||
|
@ -22250,6 +22172,109 @@ package body Sem_Prag is
|
|||
end if;
|
||||
end Check_Dependency_Clause;
|
||||
|
||||
-------------------------
|
||||
-- Check_Output_States --
|
||||
-------------------------
|
||||
|
||||
procedure Check_Output_States is
|
||||
procedure Check_Constituent_Usage (State_Id : Entity_Id);
|
||||
-- Determine whether all constituents of state State_Id with visible
|
||||
-- refinement are used as outputs in pragma Refined_Depends. Emit an
|
||||
-- error if this is not the case.
|
||||
|
||||
-----------------------------
|
||||
-- Check_Constituent_Usage --
|
||||
-----------------------------
|
||||
|
||||
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
|
||||
Constit_Elmt : Elmt_Id;
|
||||
Constit_Id : Entity_Id;
|
||||
Posted : Boolean := False;
|
||||
|
||||
begin
|
||||
Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
|
||||
while Present (Constit_Elmt) loop
|
||||
Constit_Id := Node (Constit_Elmt);
|
||||
|
||||
-- The constituent acts as an input (SPARK RM 7.2.5(3))
|
||||
|
||||
if Present (Body_Inputs)
|
||||
and then Appears_In (Body_Inputs, Constit_Id)
|
||||
then
|
||||
Error_Msg_Name_1 := Chars (State_Id);
|
||||
SPARK_Msg_NE
|
||||
("constituent & of state % must act as output in "
|
||||
& "dependence refinement", N, Constit_Id);
|
||||
|
||||
-- The constituent is altogether missing (SPARK RM 7.2.5(3))
|
||||
|
||||
elsif No (Body_Outputs)
|
||||
or else not Appears_In (Body_Outputs, Constit_Id)
|
||||
then
|
||||
if not Posted then
|
||||
Posted := True;
|
||||
SPARK_Msg_NE
|
||||
("output state & must be replaced by all its "
|
||||
& "constituents in dependence refinement",
|
||||
N, State_Id);
|
||||
end if;
|
||||
|
||||
SPARK_Msg_NE
|
||||
("\constituent & is missing in output list",
|
||||
N, Constit_Id);
|
||||
end if;
|
||||
|
||||
Next_Elmt (Constit_Elmt);
|
||||
end loop;
|
||||
end Check_Constituent_Usage;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Item : Node_Id;
|
||||
Item_Elmt : Elmt_Id;
|
||||
Item_Id : Entity_Id;
|
||||
|
||||
-- Start of processing for Check_Output_States
|
||||
|
||||
begin
|
||||
-- Inspect the outputs of pragma Depends looking for a state with a
|
||||
-- visible refinement.
|
||||
|
||||
if Present (Spec_Outputs) then
|
||||
Item_Elmt := First_Elmt (Spec_Outputs);
|
||||
while Present (Item_Elmt) loop
|
||||
Item := Node (Item_Elmt);
|
||||
|
||||
-- Deal with the mixed nature of the input and output lists
|
||||
|
||||
if Nkind (Item) = N_Defining_Identifier then
|
||||
Item_Id := Item;
|
||||
else
|
||||
Item_Id := Available_View (Entity_Of (Item));
|
||||
end if;
|
||||
|
||||
if Ekind (Item_Id) = E_Abstract_State then
|
||||
|
||||
-- The state acts as an input-output, skip it
|
||||
|
||||
if Present (Spec_Inputs)
|
||||
and then Appears_In (Spec_Inputs, Item_Id)
|
||||
then
|
||||
null;
|
||||
|
||||
-- Ensure that all of the constituents are utilized as
|
||||
-- outputs in pragma Refined_Depends.
|
||||
|
||||
elsif Has_Non_Null_Refinement (Item_Id) then
|
||||
Check_Constituent_Usage (Item_Id);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next_Elmt (Item_Elmt);
|
||||
end loop;
|
||||
end if;
|
||||
end Check_Output_States;
|
||||
|
||||
-----------------------
|
||||
-- Normalize_Clauses --
|
||||
-----------------------
|
||||
|
@ -22265,6 +22290,15 @@ package body Sem_Prag is
|
|||
-- Output => Input_1 -- normalizations
|
||||
-- Output => Input_2
|
||||
|
||||
procedure Normalize_Outputs (Clause : Node_Id);
|
||||
-- Normalize clause Clause by creating multiple clause for each
|
||||
-- output item of Clause. The transformation is as follows:
|
||||
--
|
||||
-- (Output_1, Output_2) => Input -- original
|
||||
--
|
||||
-- Output_1 => Input -- normalization
|
||||
-- Output_2 => Input
|
||||
|
||||
----------------------
|
||||
-- Normalize_Inputs --
|
||||
----------------------
|
||||
|
@ -22324,6 +22358,68 @@ package body Sem_Prag is
|
|||
end if;
|
||||
end Normalize_Inputs;
|
||||
|
||||
-----------------------
|
||||
-- Normalize_Outputs --
|
||||
-----------------------
|
||||
|
||||
procedure Normalize_Outputs (Clause : Node_Id) is
|
||||
Inputs : constant Node_Id := Expression (Clause);
|
||||
Loc : constant Source_Ptr := Sloc (Clause);
|
||||
Outputs : constant Node_Id := First (Choices (Clause));
|
||||
Last_Output : Node_Id;
|
||||
New_Clause : Node_Id;
|
||||
Next_Output : Node_Id;
|
||||
Output : Node_Id;
|
||||
|
||||
begin
|
||||
-- Multiple outputs appear as an aggregate. Nothing to do when
|
||||
-- the clause has exactly one output.
|
||||
|
||||
if Nkind (Outputs) = N_Aggregate then
|
||||
Last_Output := Last (Expressions (Outputs));
|
||||
|
||||
-- Create a clause for each output. Note that each time a new
|
||||
-- clause is created, the original output list slowly shrinks
|
||||
-- until there is one item left.
|
||||
|
||||
Output := First (Expressions (Outputs));
|
||||
while Present (Output) loop
|
||||
Next_Output := Next (Output);
|
||||
|
||||
-- Unhook the output from the original output list as it
|
||||
-- will be relocated to a new clause.
|
||||
|
||||
Remove (Output);
|
||||
|
||||
-- Special processing for the last output. At this point
|
||||
-- the original aggregate has been stripped down to one
|
||||
-- element. Replace the aggregate by the element itself.
|
||||
|
||||
if Output = Last_Output then
|
||||
Rewrite (Outputs, Output);
|
||||
|
||||
else
|
||||
-- Generate a clause of the form:
|
||||
-- (Output => Inputs)
|
||||
|
||||
New_Clause :=
|
||||
Make_Component_Association (Loc,
|
||||
Choices => New_List (Output),
|
||||
Expression => New_Copy_Tree (Inputs));
|
||||
|
||||
-- The new clause contains replicated content that has
|
||||
-- already been analyzed. There is not need to reanalyze
|
||||
-- them.
|
||||
|
||||
Set_Analyzed (New_Clause);
|
||||
Insert_After (Clause, New_Clause);
|
||||
end if;
|
||||
|
||||
Output := Next_Output;
|
||||
end loop;
|
||||
end if;
|
||||
end Normalize_Outputs;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Clause : Node_Id;
|
||||
|
@ -22331,6 +22427,12 @@ package body Sem_Prag is
|
|||
-- Start of processing for Normalize_Clauses
|
||||
|
||||
begin
|
||||
Clause := First (Clauses);
|
||||
while Present (Clause) loop
|
||||
Normalize_Outputs (Clause);
|
||||
Next (Clause);
|
||||
end loop;
|
||||
|
||||
Clause := First (Clauses);
|
||||
while Present (Clause) loop
|
||||
Normalize_Inputs (Clause);
|
||||
|
@ -22368,12 +22470,14 @@ package body Sem_Prag is
|
|||
|
||||
-- Local variables
|
||||
|
||||
Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Errors : constant Nat := Serious_Errors_Detected;
|
||||
Refs : constant Node_Id :=
|
||||
Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
|
||||
Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
|
||||
Errors : constant Nat := Serious_Errors_Detected;
|
||||
Refs : constant Node_Id :=
|
||||
Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
|
||||
Clause : Node_Id;
|
||||
Deps : Node_Id;
|
||||
Dummy : Boolean;
|
||||
|
||||
-- Start of processing for Analyze_Refined_Depends_In_Decl_Part
|
||||
|
||||
|
@ -22417,11 +22521,43 @@ package body Sem_Prag is
|
|||
Analyze_Depends_In_Decl_Part (N);
|
||||
|
||||
-- Do not match dependencies against refinements if Refined_Depends is
|
||||
-- illegal to avoid emitting misleading error. Matching is disabled in
|
||||
-- ASIS because clauses are not normalized as this is a tree altering
|
||||
-- activity similar to expansion.
|
||||
-- illegal to avoid emitting misleading error.
|
||||
|
||||
if Serious_Errors_Detected = Errors and then not ASIS_Mode then
|
||||
if Serious_Errors_Detected = Errors then
|
||||
|
||||
-- The related subprogram lacks pragma [Refined_]Global. Synthesize
|
||||
-- the inputs and outputs of the subprogram spec and body to verify
|
||||
-- the use of states with visible refinement and their constituents.
|
||||
|
||||
if No (Get_Pragma (Spec_Id, Pragma_Global))
|
||||
or else No (Get_Pragma (Body_Id, Pragma_Refined_Global))
|
||||
then
|
||||
Collect_Subprogram_Inputs_Outputs
|
||||
(Subp_Id => Spec_Id,
|
||||
Synthesize => True,
|
||||
Subp_Inputs => Spec_Inputs,
|
||||
Subp_Outputs => Spec_Outputs,
|
||||
Global_Seen => Dummy);
|
||||
|
||||
Collect_Subprogram_Inputs_Outputs
|
||||
(Subp_Id => Body_Id,
|
||||
Synthesize => True,
|
||||
Subp_Inputs => Body_Inputs,
|
||||
Subp_Outputs => Body_Outputs,
|
||||
Global_Seen => Dummy);
|
||||
|
||||
-- For an output state with a visible refinement, ensure that all
|
||||
-- constituents appear as outputs in the dependency refinement.
|
||||
|
||||
Check_Output_States;
|
||||
end if;
|
||||
|
||||
-- Matching is disabled in ASIS because clauses are not normalized as
|
||||
-- this is a tree altering activity similar to expansion.
|
||||
|
||||
if ASIS_Mode then
|
||||
return;
|
||||
end if;
|
||||
|
||||
-- Multiple dependency clauses appear as component associations of an
|
||||
-- aggregate. Note that the clauses are copied because the algorithm
|
||||
|
@ -22533,6 +22669,14 @@ package body Sem_Prag is
|
|||
-- Verify the legality of a single global list declaration. Global_Mode
|
||||
-- denotes the current mode in effect.
|
||||
|
||||
procedure Collect_Global_Items (Prag : Node_Id);
|
||||
-- Gather all input, in out, output and Proof_In items of pragma Prag
|
||||
-- in lists In_Items, In_Out_Items, Out_Items and Proof_In_Items. Flags
|
||||
-- Has_In_State, Has_In_Out_State, Has_Out_State and Has_Proof_In_State
|
||||
-- are set when there is at least one abstract state with visible
|
||||
-- refinement available in the corresponding mode. Flag Has_Null_State
|
||||
-- is set when at least state has a null refinement.
|
||||
|
||||
function Present_Then_Remove
|
||||
(List : Elist_Id;
|
||||
Item : Entity_Id) return Boolean;
|
||||
|
@ -23068,6 +23212,142 @@ package body Sem_Prag is
|
|||
end if;
|
||||
end Check_Refined_Global_List;
|
||||
|
||||
--------------------------
|
||||
-- Collect_Global_Items --
|
||||
--------------------------
|
||||
|
||||
procedure Collect_Global_Items (Prag : Node_Id) is
|
||||
procedure Process_Global_List
|
||||
(List : Node_Id;
|
||||
Mode : Name_Id := Name_Input);
|
||||
-- Collect all items housed in a global list. Formal Mode denotes the
|
||||
-- current mode in effect.
|
||||
|
||||
-------------------------
|
||||
-- Process_Global_List --
|
||||
-------------------------
|
||||
|
||||
procedure Process_Global_List
|
||||
(List : Node_Id;
|
||||
Mode : Name_Id := Name_Input)
|
||||
is
|
||||
procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id);
|
||||
-- Add a single item to the appropriate list. Formal Mode denotes
|
||||
-- the current mode in effect.
|
||||
|
||||
-------------------------
|
||||
-- Process_Global_Item --
|
||||
-------------------------
|
||||
|
||||
procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id) is
|
||||
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
|
||||
-- state with a visible refinement. Note that the refinement
|
||||
-- may be null in which case there are no constituents.
|
||||
|
||||
if Ekind (Item_Id) = E_Abstract_State then
|
||||
if Has_Null_Refinement (Item_Id) then
|
||||
Has_Null_State := True;
|
||||
|
||||
elsif Has_Non_Null_Refinement (Item_Id) then
|
||||
if Mode = Name_Input then
|
||||
Has_In_State := True;
|
||||
elsif Mode = Name_In_Out then
|
||||
Has_In_Out_State := True;
|
||||
elsif Mode = Name_Output then
|
||||
Has_Out_State := True;
|
||||
elsif Mode = Name_Proof_In then
|
||||
Has_Proof_In_State := True;
|
||||
end if;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Add the item to the proper list
|
||||
|
||||
if Mode = Name_Input then
|
||||
Add_Item (Item_Id, In_Items);
|
||||
elsif Mode = Name_In_Out then
|
||||
Add_Item (Item_Id, In_Out_Items);
|
||||
elsif Mode = Name_Output then
|
||||
Add_Item (Item_Id, Out_Items);
|
||||
elsif Mode = Name_Proof_In then
|
||||
Add_Item (Item_Id, Proof_In_Items);
|
||||
end if;
|
||||
end Process_Global_Item;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Item : Node_Id;
|
||||
|
||||
-- Start of processing for Process_Global_List
|
||||
|
||||
begin
|
||||
if Nkind (List) = N_Null then
|
||||
null;
|
||||
|
||||
-- Single global item declaration
|
||||
|
||||
elsif Nkind_In (List, N_Expanded_Name,
|
||||
N_Identifier,
|
||||
N_Selected_Component)
|
||||
then
|
||||
Process_Global_Item (List, Mode);
|
||||
|
||||
-- Single global list or moded global list declaration
|
||||
|
||||
elsif Nkind (List) = N_Aggregate then
|
||||
|
||||
-- The declaration of a simple global list appear as a
|
||||
-- collection of expressions.
|
||||
|
||||
if Present (Expressions (List)) then
|
||||
Item := First (Expressions (List));
|
||||
while Present (Item) loop
|
||||
Process_Global_Item (Item, Mode);
|
||||
Next (Item);
|
||||
end loop;
|
||||
|
||||
-- The declaration of a moded global list appears as a
|
||||
-- collection of component associations where individual
|
||||
-- choices denote mode.
|
||||
|
||||
elsif Present (Component_Associations (List)) then
|
||||
Item := First (Component_Associations (List));
|
||||
while Present (Item) loop
|
||||
Process_Global_List
|
||||
(List => Expression (Item),
|
||||
Mode => Chars (First (Choices (Item))));
|
||||
|
||||
Next (Item);
|
||||
end loop;
|
||||
|
||||
-- Invalid tree
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- To accomodate partial decoration of disabled SPARK features,
|
||||
-- this routine may be called with illegal input. If this is the
|
||||
-- case, do not raise Program_Error.
|
||||
|
||||
else
|
||||
null;
|
||||
end if;
|
||||
end Process_Global_List;
|
||||
|
||||
-- Start of processing for Collect_Global_Items
|
||||
|
||||
begin
|
||||
Process_Global_List
|
||||
(Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))));
|
||||
end Collect_Global_Items;
|
||||
|
||||
-------------------------
|
||||
-- Present_Then_Remove --
|
||||
-------------------------
|
||||
|
@ -23159,17 +23439,7 @@ package body Sem_Prag is
|
|||
|
||||
-- Extract all relevant items from the corresponding Global pragma
|
||||
|
||||
Collect_Global_Items
|
||||
(Prag => Global,
|
||||
In_Items => In_Items,
|
||||
In_Out_Items => In_Out_Items,
|
||||
Out_Items => Out_Items,
|
||||
Proof_In_Items => Proof_In_Items,
|
||||
Has_In_State => Has_In_State,
|
||||
Has_In_Out_State => Has_In_Out_State,
|
||||
Has_Out_State => Has_Out_State,
|
||||
Has_Proof_In_State => Has_Proof_In_State,
|
||||
Has_Null_State => Has_Null_State);
|
||||
Collect_Global_Items (Global);
|
||||
|
||||
-- Corresponding Global pragma must mention at least one state witha
|
||||
-- visible refinement at the point Refined_Global is processed. States
|
||||
|
@ -24638,135 +24908,89 @@ package body Sem_Prag is
|
|||
end loop;
|
||||
end Check_State_And_Constituent_Use;
|
||||
|
||||
--------------------------
|
||||
-- Collect_Global_Items --
|
||||
--------------------------
|
||||
---------------------------------------
|
||||
-- Collect_Subprogram_Inputs_Outputs --
|
||||
---------------------------------------
|
||||
|
||||
procedure Collect_Global_Items
|
||||
(Prag : Node_Id;
|
||||
In_Items : in out Elist_Id;
|
||||
In_Out_Items : in out Elist_Id;
|
||||
Out_Items : in out Elist_Id;
|
||||
Proof_In_Items : in out Elist_Id;
|
||||
Has_In_State : out Boolean;
|
||||
Has_In_Out_State : out Boolean;
|
||||
Has_Out_State : out Boolean;
|
||||
Has_Proof_In_State : out Boolean;
|
||||
Has_Null_State : out Boolean)
|
||||
procedure Collect_Subprogram_Inputs_Outputs
|
||||
(Subp_Id : Entity_Id;
|
||||
Synthesize : Boolean := False;
|
||||
Subp_Inputs : in out Elist_Id;
|
||||
Subp_Outputs : in out Elist_Id;
|
||||
Global_Seen : out Boolean)
|
||||
is
|
||||
procedure Process_Global_List
|
||||
procedure Collect_Dependency_Clause (Clause : Node_Id);
|
||||
-- Collect all relevant items from a dependency clause
|
||||
|
||||
procedure Collect_Global_List
|
||||
(List : Node_Id;
|
||||
Mode : Name_Id := Name_Input);
|
||||
-- Collect all items housed in a global list. Formal Mode denotes the
|
||||
-- current mode in effect.
|
||||
-- Collect all relevant items from a global list
|
||||
|
||||
-------------------------
|
||||
-- Process_Global_List --
|
||||
-------------------------
|
||||
-------------------------------
|
||||
-- Collect_Dependency_Clause --
|
||||
-------------------------------
|
||||
|
||||
procedure Process_Global_List
|
||||
(List : Node_Id;
|
||||
Mode : Name_Id := Name_Input)
|
||||
is
|
||||
procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id);
|
||||
-- Add a single item to the appropriate list. Formal Mode denotes the
|
||||
-- current mode in effect.
|
||||
procedure Collect_Dependency_Clause (Clause : Node_Id) is
|
||||
procedure Collect_Dependency_Item
|
||||
(Item : Node_Id;
|
||||
Is_Input : Boolean);
|
||||
-- Add an item to the proper subprogram input or output collection
|
||||
|
||||
-------------------------
|
||||
-- Process_Global_Item --
|
||||
-------------------------
|
||||
-----------------------------
|
||||
-- Collect_Dependency_Item --
|
||||
-----------------------------
|
||||
|
||||
procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id) is
|
||||
Item_Id : constant Entity_Id := Available_View (Entity_Of (Item));
|
||||
-- The above handles abstract views of variables and states built
|
||||
-- for limited with clauses.
|
||||
procedure Collect_Dependency_Item
|
||||
(Item : Node_Id;
|
||||
Is_Input : Boolean)
|
||||
is
|
||||
Extra : Node_Id;
|
||||
|
||||
begin
|
||||
-- Signal that the global list contains at least one abstract
|
||||
-- state with a visible refinement. Note that the refinement may
|
||||
-- be null in which case there are no constituents.
|
||||
-- Nothing to collect when the item is null
|
||||
|
||||
if Ekind (Item_Id) = E_Abstract_State then
|
||||
if Has_Null_Refinement (Item_Id) then
|
||||
Has_Null_State := True;
|
||||
if Nkind (Item) = N_Null then
|
||||
null;
|
||||
|
||||
elsif Has_Non_Null_Refinement (Item_Id) then
|
||||
if Mode = Name_Input then
|
||||
Has_In_State := True;
|
||||
elsif Mode = Name_In_Out then
|
||||
Has_In_Out_State := True;
|
||||
elsif Mode = Name_Output then
|
||||
Has_Out_State := True;
|
||||
elsif Mode = Name_Proof_In then
|
||||
Has_Proof_In_State := True;
|
||||
end if;
|
||||
end if;
|
||||
end if;
|
||||
-- Ditto for attribute 'Result
|
||||
|
||||
-- Add the item to the proper list
|
||||
elsif Is_Attribute_Result (Item) then
|
||||
null;
|
||||
|
||||
if Mode = Name_Input then
|
||||
Add_Item (Item_Id, In_Items);
|
||||
elsif Mode = Name_In_Out then
|
||||
Add_Item (Item_Id, In_Out_Items);
|
||||
elsif Mode = Name_Output then
|
||||
Add_Item (Item_Id, Out_Items);
|
||||
elsif Mode = Name_Proof_In then
|
||||
Add_Item (Item_Id, Proof_In_Items);
|
||||
end if;
|
||||
end Process_Global_Item;
|
||||
-- Multiple items appear as an aggregate
|
||||
|
||||
-- Local variables
|
||||
|
||||
Item : Node_Id;
|
||||
|
||||
-- Start of processing for Process_Global_List
|
||||
|
||||
begin
|
||||
if Nkind (List) = N_Null then
|
||||
null;
|
||||
|
||||
-- Single global item declaration
|
||||
|
||||
elsif Nkind_In (List, N_Expanded_Name,
|
||||
N_Identifier,
|
||||
N_Selected_Component)
|
||||
then
|
||||
Process_Global_Item (List, Mode);
|
||||
|
||||
-- Single global list or moded global list declaration
|
||||
|
||||
elsif Nkind (List) = N_Aggregate then
|
||||
|
||||
-- The declaration of a simple global list appear as a collection
|
||||
-- of expressions.
|
||||
|
||||
if Present (Expressions (List)) then
|
||||
Item := First (Expressions (List));
|
||||
while Present (Item) loop
|
||||
Process_Global_Item (Item, Mode);
|
||||
|
||||
Next (Item);
|
||||
elsif Nkind (Item) = N_Aggregate then
|
||||
Extra := First (Expressions (Item));
|
||||
while Present (Extra) loop
|
||||
Collect_Dependency_Item (Extra, Is_Input);
|
||||
Next (Extra);
|
||||
end loop;
|
||||
|
||||
-- The declaration of a moded global list appears as a collection
|
||||
-- of component associations where individual choices denote mode.
|
||||
|
||||
elsif Present (Component_Associations (List)) then
|
||||
Item := First (Component_Associations (List));
|
||||
while Present (Item) loop
|
||||
Process_Global_List
|
||||
(List => Expression (Item),
|
||||
Mode => Chars (First (Choices (Item))));
|
||||
|
||||
Next (Item);
|
||||
end loop;
|
||||
|
||||
-- Invalid tree
|
||||
-- Otherwise this is a solitary item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
if Is_Input then
|
||||
Add_Item (Item, Subp_Inputs);
|
||||
else
|
||||
Add_Item (Item, Subp_Outputs);
|
||||
end if;
|
||||
end if;
|
||||
end Collect_Dependency_Item;
|
||||
|
||||
-- Start of processing for Collect_Dependency_Clause
|
||||
|
||||
begin
|
||||
if Nkind (Clause) = N_Null then
|
||||
null;
|
||||
|
||||
-- A dependency cause appears as component association
|
||||
|
||||
elsif Nkind (Clause) = N_Component_Association then
|
||||
Collect_Dependency_Item
|
||||
(Expression (Clause), Is_Input => True);
|
||||
Collect_Dependency_Item
|
||||
(First (Choices (Clause)), Is_Input => False);
|
||||
|
||||
-- To accomodate partial decoration of disabled SPARK features, this
|
||||
-- routine may be called with illegal input. If this is the case, do
|
||||
|
@ -24775,41 +24999,7 @@ package body Sem_Prag is
|
|||
else
|
||||
null;
|
||||
end if;
|
||||
end Process_Global_List;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Items : constant Node_Id :=
|
||||
Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
|
||||
|
||||
-- Start of processing for Collect_Global_Items
|
||||
|
||||
begin
|
||||
-- Assume that no states have been encountered
|
||||
|
||||
Has_In_State := False;
|
||||
Has_In_Out_State := False;
|
||||
Has_Out_State := False;
|
||||
Has_Proof_In_State := False;
|
||||
Has_Null_State := False;
|
||||
|
||||
Process_Global_List (Items);
|
||||
end Collect_Global_Items;
|
||||
|
||||
---------------------------------------
|
||||
-- Collect_Subprogram_Inputs_Outputs --
|
||||
---------------------------------------
|
||||
|
||||
procedure Collect_Subprogram_Inputs_Outputs
|
||||
(Subp_Id : Entity_Id;
|
||||
Subp_Inputs : in out Elist_Id;
|
||||
Subp_Outputs : in out Elist_Id;
|
||||
Global_Seen : out Boolean)
|
||||
is
|
||||
procedure Collect_Global_List
|
||||
(List : Node_Id;
|
||||
Mode : Name_Id := Name_Input);
|
||||
-- Collect all relevant items from a global list
|
||||
end Collect_Dependency_Clause;
|
||||
|
||||
-------------------------
|
||||
-- Collect_Global_List --
|
||||
|
@ -24887,7 +25077,10 @@ package body Sem_Prag is
|
|||
|
||||
-- Local variables
|
||||
|
||||
Subp_Decl : constant Node_Id := Parent (Parent (Subp_Id));
|
||||
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
|
||||
Clause : Node_Id;
|
||||
Clauses : Node_Id;
|
||||
Depends : Node_Id;
|
||||
Formal : Entity_Id;
|
||||
Global : Node_Id;
|
||||
List : Node_Id;
|
||||
|
@ -24939,18 +25132,23 @@ package body Sem_Prag is
|
|||
Next_Formal (Formal);
|
||||
end loop;
|
||||
|
||||
-- When processing a subprogram body, look for pragma Refined_Global as
|
||||
-- it provides finer granularity of inputs and outputs.
|
||||
-- When processing a subprogram body, look for pragmas Refined_Depends
|
||||
-- and Refined_Global as they specify the inputs and outputs.
|
||||
|
||||
if Ekind (Subp_Id) = E_Subprogram_Body then
|
||||
Global := Get_Pragma (Subp_Id, Pragma_Refined_Global);
|
||||
Depends := Get_Pragma (Subp_Id, Pragma_Refined_Depends);
|
||||
Global := Get_Pragma (Subp_Id, Pragma_Refined_Global);
|
||||
|
||||
-- Subprogram declaration case, look for pragma Global
|
||||
-- Subprogram declaration case, look for pragmas Depends and Global
|
||||
|
||||
else
|
||||
Global := Get_Pragma (Spec_Id, Pragma_Global);
|
||||
Depends := Get_Pragma (Spec_Id, Pragma_Depends);
|
||||
Global := Get_Pragma (Spec_Id, Pragma_Global);
|
||||
end if;
|
||||
|
||||
-- Pragma [Refined_]Global takes precedence over [Refined_]Depends
|
||||
-- because it provides finer granularity of inputs and outputs.
|
||||
|
||||
if Present (Global) then
|
||||
Global_Seen := True;
|
||||
List := Expression (First (Pragma_Argument_Associations (Global)));
|
||||
|
@ -24967,10 +25165,29 @@ package body Sem_Prag is
|
|||
end if;
|
||||
end if;
|
||||
|
||||
-- Nothing to be done for a null global list
|
||||
Collect_Global_List (List);
|
||||
|
||||
if Nkind (List) /= N_Null then
|
||||
Collect_Global_List (List);
|
||||
-- When the related subprogram lacks pragma [Refined_]Global, fall back
|
||||
-- to [Refined_]Depends if the caller requests this behavior. Synthesize
|
||||
-- the inputs and outputs from [Refined_]Depends.
|
||||
|
||||
elsif Synthesize and then Present (Depends) then
|
||||
Clauses :=
|
||||
Get_Pragma_Arg (First (Pragma_Argument_Associations (Depends)));
|
||||
|
||||
-- Multiple dependency clauses appear as an aggregate
|
||||
|
||||
if Nkind (Clauses) = N_Aggregate then
|
||||
Clause := First (Component_Associations (Clauses));
|
||||
while Present (Clause) loop
|
||||
Collect_Dependency_Clause (Clause);
|
||||
Next (Clause);
|
||||
end loop;
|
||||
|
||||
-- Otherwise this is a single dependency clause
|
||||
|
||||
else
|
||||
Collect_Dependency_Clause (Clauses);
|
||||
end if;
|
||||
end if;
|
||||
end Collect_Subprogram_Inputs_Outputs;
|
||||
|
|
|
@ -172,14 +172,21 @@ package Sem_Prag is
|
|||
|
||||
procedure Collect_Subprogram_Inputs_Outputs
|
||||
(Subp_Id : Entity_Id;
|
||||
Synthesize : Boolean := False;
|
||||
Subp_Inputs : in out Elist_Id;
|
||||
Subp_Outputs : in out Elist_Id;
|
||||
Global_Seen : out Boolean);
|
||||
-- Used during the analysis of pragmas Depends, Global, Refined_Depends,
|
||||
-- and Refined_Global. Also used by GNATprove. Gathers all inputs and
|
||||
-- outputs of subprogram Subp_Id in lists Subp_Inputs and Subp_Outputs.
|
||||
-- If subprogram has no inputs and/or outputs, then the returned list
|
||||
-- is No_Elist. Global_Seen is set when the related subprogram has
|
||||
-- Subsidiary to the analysis of pragmas Depends, Global, Refined_Depends
|
||||
-- and Refined_Global. The routine is also used by GNATprove. Collect all
|
||||
-- inputs and outputs of subprogram Subp_Id in lists Subp_Inputs (inputs)
|
||||
-- and Subp_Outputs (outputs). The inputs and outputs are gathered from:
|
||||
-- 1) The formal parameters of the subprogram
|
||||
-- 2) The items of pragma [Refined_]Global
|
||||
-- or
|
||||
-- 3) The items of pragma [Refined_]Depends if there is no pragma
|
||||
-- [Refined_]Global present and flag Synthesize is set to True.
|
||||
-- If the subprogram has no inputs and/or outputs, then the returned list
|
||||
-- is No_Elist. Flag Global_Seen is set when the related subprogram has
|
||||
-- pragma [Refined_]Global.
|
||||
|
||||
function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean;
|
||||
|
|
Loading…
Reference in New Issue