[COMMITTED] ada: Fix spurious error in checking of SPARK elaboration

Message ID 20221206140211.717323-1-poulhies@adacore.com
State Committed
Commit 0cb36c85ab0c9876dde207d5b93aad7398539c7e
Headers
Series [COMMITTED] ada: Fix spurious error in checking of SPARK elaboration |

Commit Message

Marc Poulhiès Dec. 6, 2022, 2:02 p.m. UTC
  From: Eric Botcazou <ebotcazou@adacore.com>

The problem is that the computation of early call regions skips freeze nodes
but scenarios involving procedures declared as actions of these freeze nodes
are taken into account.  As a consequence if a subprogram body, typically of
an expression function, is placed just after a freeze node, its early call
region depends on whether the construct just before the freeze node can be
preelaborated or not; in other words, the legality of calls made from the
actions of this freeze node to the subprogram depends on what happens ahead
of the freeze node, which may be totally unrelated to the situation.

This change disables the ABE diagnostics in this case, as is done in a few
other similar cases leading to bogus errors too.

gcc/ada/

	* sem_elab.adb (Processing_In_State): Add Within_Freezing_Actions
	component.
	(Process_Conditional_ABE_Call): Compute its value.
	(Process_Conditional_ABE_Call_SPARK): For a call and a target in
	the main unit, do not emit any ABE diagnostics if the call occurs
	in a freezing actions context.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/sem_elab.adb | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)
  

Patch

diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index a1e8f1ef30b..9bf8614fd52 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -881,6 +881,10 @@  package body Sem_Elab is
       --  The subprogram body traversal mode. Once set, this value should not
       --  be changed.
 
+      Within_Freezing_Actions : Boolean := False;
+      --  This flag is set when the Processing phase is currently examining a
+      --  scenario which was reached from the actions of a freeze node.
+
       Within_Generic : Boolean := False;
       --  This flag is set when the Processing phase is currently within a
       --  generic unit.
@@ -5353,6 +5357,7 @@  package body Sem_Elab is
          Subp_Id   : constant Entity_Id     := Target (Call_Rep);
          Subp_Rep  : constant Target_Rep_Id :=
                        Target_Representation_Of (Subp_Id, In_State);
+         Body_Decl : constant Node_Id       := Body_Declaration (Subp_Rep);
          Subp_Decl : constant Node_Id       := Spec_Declaration (Subp_Rep);
 
          SPARK_Rules_On : constant Boolean :=
@@ -5452,6 +5457,16 @@  package body Sem_Elab is
              or else not Elaboration_Warnings_OK (Call_Rep)
              or else not Elaboration_Warnings_OK (Subp_Rep);
 
+         --  The call occurs in freezing actions context when a prior scenario
+         --  is already in that mode, or when the target is a subprogram whose
+         --  body has been generated as a freezing action. Update the state of
+         --  the Processing phase to reflect this.
+
+         New_In_State.Within_Freezing_Actions :=
+           New_In_State.Within_Freezing_Actions
+             or else (Present (Body_Decl)
+                       and then Nkind (Parent (Body_Decl)) = N_Freeze_Entity);
+
          --  The call occurs in an initial condition context when a prior
          --  scenario is already in that mode, or when the target is an
          --  Initial_Condition procedure. Update the state of the Processing
@@ -5502,7 +5517,7 @@  package body Sem_Elab is
             In_State => New_In_State);
 
          Traverse_Conditional_ABE_Body
-           (N        => Body_Declaration (Subp_Rep),
+           (N        => Body_Decl,
             In_State => New_In_State);
       end Process_Conditional_ABE_Call;
 
@@ -5721,6 +5736,13 @@  package body Sem_Elab is
             if In_State.Suppress_Warnings then
                null;
 
+            --  Do not emit any ABE diagnostics when the call occurs in a
+            --  freezing actions context because this leads to incorrect
+            --  diagnostics.
+
+            elsif In_State.Within_Freezing_Actions then
+               null;
+
             --  Do not emit any ABE diagnostics when the call occurs in an
             --  initial condition context because this leads to incorrect
             --  diagnostics.