This patch updates the analysis of aspect/pragma Depends to verify the legality
of a self-referential output.
------------
-- Source --
------------
-- semantics.ads
package Semantics
with Abstract_State =>
((Input_State with Volatile, Input),
(Output_State with Volatile, Output))
is
Input_Var : Integer; -- in
Mixed_Var : Integer; -- in out
Output_Var : Integer; -- out
procedure Error (Formal : out Integer) with
Global =>
(Input =>
(Input_State, Input_Var),
Output =>
(Output_State, Output_Var),
In_Out =>
Mixed_Var),
Depends =>
((Formal, -- error
Mixed_Var, -- ok, already in out
Output_State, -- error
Output_Var) -- error
=>+ (Input_Var,
Input_State,
Mixed_Var));
end Semantics;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnat12 -gnatd.V semantics.ads
semantics.ads:20:10: item "Formal" must have mode in out
semantics.ads:22:10: item "Output_State" must have mode in out
semantics.ads:23:10: item "Output_Var" must have mode in out
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-04-23 Hristian Kirtchev <kirtc...@adacore.com>
* sem_prag.adb (Analyze_Dependency_Clause): Update all calls to
Analyze_Input_Output.
(Analyze_Input_List): Update all calls to Analyze_Input_Output.
(Analyze_Input_Output): Add formal parameter Self_Ref along with
comment on its usage. Update all calls to Analyze_Input_Output.
(Analyze_Pragma): Add new local variable Self_Ref to capture
the presence of a self-referential dependency clause. Update
all calls to Analyze_Input_Output.
(Check_Mode): Add formal parameter Self_Ref along with comment on its
usage. Verify the legality of a self-referential output.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 198175)
+++ sem_prag.adb (working copy)
@@ -9346,10 +9346,14 @@
procedure Check_Mode
(Item : Node_Id;
Item_Id : Entity_Id;
- Is_Input : Boolean);
+ Is_Input : Boolean;
+ Self_Ref : Boolean);
-- Ensure that an item has a proper "in", "in out" or "out" mode
-- depending on its function. If this is not the case, emit an
- -- error.
+ -- error. Item and Item_Id denote the attributes of an item. Flag
+ -- Is_Input should be set when item comes from an input list.
+ -- Flag Self_Ref should be set when the item is an output and the
+ -- dependency clause has operator "+".
procedure Check_Usage
(Subp_List : Elist_Id;
@@ -9382,16 +9386,19 @@
procedure Analyze_Input_Output
(Item : Node_Id;
Is_Input : Boolean;
+ Self_Ref : Boolean;
Top_Level : Boolean;
Seen : in out Elist_Id;
Null_Seen : in out Boolean);
-- Verify the legality of a single input or output item. Flag
-- Is_Input should be set whenever Item is an input, False when
- -- it denotes an output. Flag Top_Level should be set whenever
- -- Item appears immediately within an input or output list.
- -- Seen is a collection of all abstract states, variables and
- -- formals processed so far. Flag Null_Seen denotes whether a
- -- null input or output has been encountered.
+ -- it denotes an output. Flag Self_Ref should be set when the
+ -- item is an output and the dependency clause has a "+". Flag
+ -- Top_Level should be set whenever Item appears immediately
+ -- within an input or output list. Seen is a collection of all
+ -- abstract states, variables and formals processed so far.
+ -- Flag Null_Seen denotes whether a null input or output has
+ -- been encountered.
------------------------
-- Analyze_Input_List --
@@ -9421,6 +9428,7 @@
Analyze_Input_Output
(Item => Input,
Is_Input => True,
+ Self_Ref => False,
Top_Level => False,
Seen => Inputs_Seen,
Null_Seen => Null_Input_Seen);
@@ -9439,6 +9447,7 @@
Analyze_Input_Output
(Item => Inputs,
Is_Input => True,
+ Self_Ref => False,
Top_Level => False,
Seen => Inputs_Seen,
Null_Seen => Null_Input_Seen);
@@ -9462,6 +9471,7 @@
procedure Analyze_Input_Output
(Item : Node_Id;
Is_Input : Boolean;
+ Self_Ref : Boolean;
Top_Level : Boolean;
Seen : in out Elist_Id;
Null_Seen : in out Boolean)
@@ -9490,6 +9500,7 @@
Analyze_Input_Output
(Item => Grouped,
Is_Input => Is_Input,
+ Self_Ref => Self_Ref,
Top_Level => False,
Seen => Seen,
Null_Seen => Null_Seen);
@@ -9576,7 +9587,7 @@
-- Ensure that the item is of the correct mode
-- depending on its function.
- Check_Mode (Item, Item_Id, Is_Input);
+ Check_Mode (Item, Item_Id, Is_Input, Self_Ref);
-- Detect multiple uses of the same state, variable
-- or formal parameter. If this is not the case,
@@ -9631,12 +9642,24 @@
-- Local variables
- Inputs : Node_Id;
- Output : Node_Id;
+ Inputs : Node_Id;
+ Output : Node_Id;
+ Self_Ref : Boolean;
-- Start of processing for Analyze_Dependency_Clause
begin
+ Inputs := Expression (Clause);
+ Self_Ref := False;
+
+ -- An input list with a self-dependency appears as operator "+"
+ -- where the actuals inputs are the right operand.
+
+ if Nkind (Inputs) = N_Op_Plus then
+ Inputs := Right_Opnd (Inputs);
+ Self_Ref := True;
+ end if;
+
-- Process the output_list of a dependency_clause
Output := First (Choices (Clause));
@@ -9644,6 +9667,7 @@
Analyze_Input_Output
(Item => Output,
Is_Input => False,
+ Self_Ref => Self_Ref,
Top_Level => True,
Seen => Outputs_Seen,
Null_Seen => Null_Output_Seen);
@@ -9653,15 +9677,6 @@
-- Process the input_list of a dependency_clause
- Inputs := Expression (Clause);
-
- -- An input list with a self-dependency appears as operator "+"
- -- where the actuals inputs are the right operand.
-
- if Nkind (Inputs) = N_Op_Plus then
- Inputs := Right_Opnd (Inputs);
- end if;
-
Analyze_Input_List (Inputs);
end Analyze_Dependency_Clause;
@@ -9717,9 +9732,12 @@
procedure Check_Mode
(Item : Node_Id;
Item_Id : Entity_Id;
- Is_Input : Boolean)
+ Is_Input : Boolean;
+ Self_Ref : Boolean)
is
begin
+ -- Input
+
if Is_Input then
if Ekind (Item_Id) = E_Out_Parameter
or else (Global_Seen
@@ -9729,17 +9747,37 @@
("item & must have mode in or in out", Item, Item_Id);
end if;
- -- Output
+ -- Self-referential output
- else
- if Ekind (Item_Id) = E_In_Parameter
- or else
- (Global_Seen
- and then not Appears_In (Subp_Outputs, Item_Id))
- then
+ elsif Self_Ref then
+
+ -- A self-referential state or variable must appear in both
+ -- input and output lists of a subprogram.
+
+ if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+ if Global_Seen
+ and then not Appears_In (Subp_Inputs, Item_Id)
+ then
+ Error_Msg_NE
+ ("item & must have mode in out", Item, Item_Id);
+ end if;
+
+ -- Self-referential parameter
+
+ elsif Ekind (Item_Id) /= E_In_Out_Parameter then
Error_Msg_NE
- ("item & must have mode out or in out", Item, Item_Id);
+ ("item & must have mode in out", Item, Item_Id);
end if;
+
+ -- Regular output
+
+ elsif Ekind (Item_Id) = E_In_Parameter
+ or else
+ (Global_Seen
+ and then not Appears_In (Subp_Outputs, Item_Id))
+ then
+ Error_Msg_NE
+ ("item & must have mode out or in out", Item, Item_Id);
end if;
end Check_Mode;
