From: Viljar Indus Date: Fri, 1 Aug 2025 06:06:29 +0000 (+0300) Subject: ada: Fix ghost policy change detection for procedure calls X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=2a30a4b62c60764938d113c6dcc628150fe78a3b;p=thirdparty%2Fgcc.git ada: Fix ghost policy change detection for procedure calls gcc/ada/ChangeLog: * ghost.adb (Check_Ghost_Policy): Use the policy in affect for the identifier at the current moment instead of the region around it when checking a policy change for a procedure call. --- diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index b055298319e..6e843bda957 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -840,8 +840,8 @@ package body Ghost is ------------------------ procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is + Applic_Policy : Ghost_Mode_Type := Ghost_Config.Ghost_Mode; Ghost_Region : constant Node_Id := Ghost_Config.Current_Region; - Region_Policy : constant Ghost_Mode_Type := Ghost_Config.Ghost_Mode; begin -- Ghost entities can be referenced inside a renaming declaration if -- used within a renaming declaration. @@ -854,11 +854,18 @@ package body Ghost is return; end if; + -- The applied policy for procedure calls is the policy in effect at + -- the moment of the call. + + if Ekind (Id) in E_Procedure then + Applic_Policy := Name_To_Ghost_Mode (Ghost_Policy_In_Effect (Id)); + end if; + -- The Ghost policy in effect a the point of declaration and at the -- point of use must match (SPARK RM 6.9(15)). if Is_Checked_Ghost_Entity (Id) - and then Region_Policy = Ignore + and then Applic_Policy = Ignore and then Known_To_Be_Assigned (Ref) then Error_Msg_N (Ghost_Policy_Error_Msg, Ref); @@ -880,7 +887,7 @@ package body Ghost is return; end if; - if Is_Ignored_Ghost_Entity (Id) and then Region_Policy = Check + if Is_Ignored_Ghost_Entity (Id) and then Applic_Policy = Check then Error_Msg_N (Ghost_Policy_Error_Msg, Ref); Error_Msg_NE ("\& declared with ghost policy `Ignore`", Ref, Id);