-- 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,
-- 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;
-- 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 --
-- 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 --
-----------------------------
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));
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
------------------------------------------
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
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
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 --
-----------------------
-- 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 --
----------------------
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;
-- 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);
-- 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
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 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.
- if Serious_Errors_Detected = Errors and then not ASIS_Mode then
+ 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
-- 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;
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 --
-------------------------
-- 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
end loop;
end Check_State_And_Constituent_Use;
- --------------------------
- -- Collect_Global_Items --
- --------------------------
-
- 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)
+ ---------------------------------------
+ -- Collect_Subprogram_Inputs_Outputs --
+ ---------------------------------------
+
+ 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.
-
- 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;
+ -- Nothing to collect when the item is null
- -- 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
+ if Nkind (Item) = N_Null then
+ null;
- elsif Nkind (List) = N_Aggregate then
+ -- Ditto for attribute 'Result
- -- The declaration of a simple global list appear as a collection
- -- of expressions.
+ elsif Is_Attribute_Result (Item) then
+ null;
- if Present (Expressions (List)) then
- Item := First (Expressions (List));
- while Present (Item) loop
- Process_Global_Item (Item, Mode);
+ -- Multiple items appear as an aggregate
- 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.
+ -- Otherwise this is a solitary item
- 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))));
+ else
+ if Is_Input then
+ Add_Item (Item, Subp_Inputs);
+ else
+ Add_Item (Item, Subp_Outputs);
+ end if;
+ end if;
+ end Collect_Dependency_Item;
- Next (Item);
- end loop;
+ -- Start of processing for Collect_Dependency_Clause
- -- Invalid tree
+ begin
+ if Nkind (Clause) = N_Null then
+ null;
- else
- raise Program_Error;
- end if;
+ -- 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
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 --
-- 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;
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)));
end if;
end if;
- -- Nothing to be done for a null global list
+ 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
- if Nkind (List) /= N_Null then
- Collect_Global_List (List);
+ else
+ Collect_Dependency_Clause (Clauses);
end if;
end if;
end Collect_Subprogram_Inputs_Outputs;
projects / gcc.git / commitdiff