From: Piotr Trojanek <troja...@adacore.com>
Add check for references to subprogram outputs occurring within the
Program_Exit expression. This check is necessarily partial, as it misses
objects referenced by subprograms called from the Program_Exit expression,
but this is consistent with other checks.
gcc/ada/ChangeLog:
* sem_prag.adb (Analyze_Pragma): Add dependency of Program_Exit on
Global and Depends contracts.
(Analyze_Program_Exit_In_Decl_Part): Check references to subprogram
outputs.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sem_prag.adb | 51 ++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 51 insertions(+)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 70681231329..b94606eabc7 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -23717,6 +23717,8 @@ package body Sem_Prag is
Analyze_If_Present (Pragma_SPARK_Mode);
Analyze_If_Present (Pragma_Volatile_Function);
+ Analyze_If_Present (Pragma_Global);
+ Analyze_If_Present (Pragma_Depends);
Analyze_Program_Exit_In_Decl_Part (N);
end if;
end Program_Exit;
@@ -28425,6 +28427,46 @@ package body Sem_Prag is
Errors : Nat;
Restore_Scope : Boolean := False;
+ Unused : Boolean;
+
+ Subp_Inputs, Subp_Outputs : Elist_Id := No_Elist;
+ -- Inputs and outputs of the subprogram
+
+ function Check_Reference (N : Node_Id) return Traverse_Result;
+ -- Check references to objects within the Program_Exit expression
+
+ ---------------------
+ -- Check_Reference --
+ ---------------------
+
+ function Check_Reference (N : Node_Id) return Traverse_Result is
+ begin
+ -- If an output of a subprogram with side effects is mentioned
+ -- in the boolean expression of its aspect Program_Exit, then it
+ -- shall either occur inside the prefix of a reference to the Old
+ -- attribute or be a stand-alone object.
+
+ if Is_Attribute_Old (N) then
+ return Skip;
+ end if;
+
+ if Is_Entity_Name (N) then
+ declare
+ E : constant Entity_Id := Entity (N);
+ begin
+ if Appears_In (Subp_Outputs, E)
+ and then Ekind (E) not in E_Constant | E_Variable
+ then
+ Error_Msg_NE
+ ("reference to subprogram output & in Program_Exit", N, E);
+ end if;
+ end;
+ end if;
+
+ return OK;
+ end Check_Reference;
+
+ procedure Check_Exit_References is new Traverse_Proc (Check_Reference);
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
@@ -28475,6 +28517,15 @@ package body Sem_Prag is
Preanalyze_And_Resolve_Assert_Expression
(Expression (Arg1), Any_Boolean);
+ Collect_Subprogram_Inputs_Outputs
+ (Spec_Id,
+ Synthesize => True,
+ Subp_Inputs => Subp_Inputs,
+ Subp_Outputs => Subp_Outputs,
+ Global_Seen => Unused);
+
+ Check_Exit_References (Expression (Arg1));
+
-- Emit a clarification message when the expression contains at least
-- one undefined reference, possibly due to contract freezing.
--
2.43.0
