https://gcc.gnu.org/g:cdc0270f93360b9bee6c3e5e07677a37315346fd
commit r15-1270-gcdc0270f93360b9bee6c3e5e07677a37315346fd
Author: Piotr Trojanek <troja...@adacore.com>
Date: Tue Apr 9 14:39:25 2024 +0200
ada: Check global mode restriction on encapsulating abstract states
We already checked that a global item of mode Output is not an Input of
the enclosing subprograms. With this change we also check that if this
global item is a constituent, then none of its encapsulating abstract
states is an Input of the enclosing subprograms.
gcc/ada/
* sem_prag.adb (Check_Mode_Restriction_In_Enclosing_Context):
Iterate over encapsulating abstract states.
Diff:
---
gcc/ada/sem_prag.adb | 81 ++++++++++++++++++++++++++++++++++++----------------
1 file changed, 56 insertions(+), 25 deletions(-)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 6d4ec122a218..d3b29089d772 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2966,16 +2966,18 @@ package body Sem_Prag is
(Item : Node_Id;
Item_Id : Entity_Id)
is
- Context : Entity_Id;
- Dummy : Boolean;
- Inputs : Elist_Id := No_Elist;
- Outputs : Elist_Id := No_Elist;
+ Context : Entity_Id;
+ Dummy : Boolean;
+ Item_View : Entity_Id;
+ Inputs : Elist_Id := No_Elist;
+ Outputs : Elist_Id := No_Elist;
begin
-- Traverse the scope stack looking for enclosing subprograms or
-- tasks subject to pragma [Refined_]Global.
Context := Scope (Subp_Id);
+ Check_Context :
while Present (Context) and then Context /= Standard_Standard loop
-- For a single task type, retrieve the corresponding object to
@@ -2997,35 +2999,64 @@ package body Sem_Prag is
Subp_Outputs => Outputs,
Global_Seen => Dummy);
- -- The item is classified as In_Out or Output but appears as
- -- an Input or a formal parameter of mode IN in an enclosing
- -- subprogram or task unit (SPARK RM 6.1.4(13)).
+ -- If the item is a constituent, we must check not just the
+ -- item itself, but also its encapsulating abstract states.
- if Appears_In (Inputs, Item_Id)
- and then not Appears_In (Outputs, Item_Id)
- then
- SPARK_Msg_NE
- ("global item & cannot have mode In_Out or Output",
- Item, Item_Id);
+ Item_View := Item_Id;
- if Is_Subprogram_Or_Entry (Context) then
- SPARK_Msg_NE
- (Fix_Msg (Subp_Id, "\item already appears as input "
- & "of subprogram &"), Item, Context);
- else
- SPARK_Msg_NE
- (Fix_Msg (Subp_Id, "\item already appears as input "
- & "of task &"), Item, Context);
+ Check_View : loop
+ -- The item is classified as In_Out or Output but appears
+ -- as an Input or a formal parameter of mode IN in
+ -- an enclosing subprogram or task unit (SPARK RM
+ -- 6.1.4(13)).
+
+ if Appears_In (Inputs, Item_View)
+ and then not Appears_In (Outputs, Item_View)
+ then
+ if Item_View = Item_Id then
+ SPARK_Msg_NE
+ ("global item & " &
+ "cannot have mode In_Out or Output",
+ Item, Item_Id);
+ else
+ Error_Msg_Node_2 := Item_View;
+ SPARK_Msg_NE
+ ("global constituent & of & " &
+ "cannot have mode In_Out or Output",
+ Item, Item_Id);
+ end if;
+
+ if Is_Subprogram_Or_Entry (Context) then
+ SPARK_Msg_NE
+ (Fix_Msg (Subp_Id, "\item already appears "
+ & "as input of subprogram &"), Item, Context);
+ else
+ SPARK_Msg_NE
+ (Fix_Msg (Subp_Id, "\item already appears "
+ & "as input of task &"), Item, Context);
+ end if;
+
+ -- Stop the traversal once an error has been detected
+
+ exit Check_Context;
end if;
- -- Stop the traversal once an error has been detected
+ if Ekind (Item_View) in E_Abstract_State
+ | E_Constant
+ | E_Variable
+ then
+ Item_View := Encapsulating_State (Item_View);
+
+ exit Check_View when No (Item_View);
+ else
+ exit Check_View;
+ end if;
+ end loop Check_View;
- exit;
- end if;
end if;
Context := Scope (Context);
- end loop;
+ end loop Check_Context;
end Check_Mode_Restriction_In_Enclosing_Context;
----------------------------------------
