-- 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.
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 :=
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
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;
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.