@@ -31608,7 +31608,7 @@ package body Sem_Prag is
Pragma_Refined_Depends => -1,
Pragma_Refined_Global => -1,
Pragma_Refined_Post => -1,
- Pragma_Refined_State => -1,
+ Pragma_Refined_State => 0,
Pragma_Relative_Deadline => 0,
Pragma_Remote_Access_Type => -1,
Pragma_Remote_Call_Interface => -1,
@@ -31713,6 +31713,15 @@ package body Sem_Prag is
P := Parent (N);
if Nkind (P) /= N_Pragma_Argument_Association then
+
+ -- References within pragma Refined_State are not significant. They
+ -- can't be recognized using pragma argument number, because they
+ -- appear inside refinement clauses that rely on aggregate syntax.
+
+ if In_Pragma_Expression (N, Name_Refined_State) then
+ return True;
+ end if;
+
return False;
else
From: Piotr Trojanek <trojanek@adacore.com> Listing an object as a state refinement constituent shouldn't be considered to be a reference, at least from the point of view of the machinery for detecting objects that are never referenced or written without being referenced. This patch fixes a spurious warning that rarely occurred in practice but was annoyingly emitted for minimal reproducers for issues related to state abstractions. Note: there are other pragmas that should be similarly recognized (e.g. Depends, Global and their refined variants), but recognizing them efficiently probably requires a dedicated utility routine (i.e. to avoid traversal of the parent chain for every kind of pragma). gcc/ada/ * sem_prag.adb (Sig_Pragma): Change flag for pragma Refined_State to mean "not significant"; this is primarily for documentation, because the exact value of the flag is not really taken into account for Refined_State. (Is_Non_Significant_Pragma_Reference): Add special handling for pragma Refined_State. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/sem_prag.adb | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-)