https://gcc.gnu.org/g:6cca06865a8ed75f8ccee9e3bea98d060104c29e
commit r16-3877-g6cca06865a8ed75f8ccee9e3bea98d060104c29e Author: Viljar Indus <[email protected]> Date: Tue Sep 2 10:30:53 2025 +0300 ada: Remove checks for the old rule 20 This rule was removed. This can scenario can be detected by Rule 18. gcc/ada/ChangeLog: * ghost.adb (Is_Ok_Pragma): Remove calls to Check_Policies. Diff: --- gcc/ada/ghost.adb | 48 +++++------------------------------------------- 1 file changed, 5 insertions(+), 43 deletions(-) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index d097c70b707f..40075bdf0a6b 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -278,9 +278,9 @@ package body Ghost is -- -- * Be subject to pragma Ghost - function Is_OK_Pragma (Prag : Node_Id; Id : Entity_Id) return Boolean; - -- Determine whether node Prag is a suitable context for a reference - -- to a Ghost entity Id. To qualify as such, Prag must either + function Is_OK_Pragma (Prag : Node_Id) return Boolean; + -- Determine whether node Prag is a suitable context for a ghost + -- reference. To qualify as such, Prag must either -- -- * Be an assertion expression pragma -- @@ -424,45 +424,11 @@ package body Ghost is -- Is_OK_Pragma -- ------------------ - function Is_OK_Pragma (Prag : Node_Id; Id : Entity_Id) return Boolean + function Is_OK_Pragma (Prag : Node_Id) return Boolean is - procedure Check_Policies; - -- Verify that the Ghost policy in effect at the point of the - -- declaration of Ghost entity Id (if present) is the same as - -- the assertion policy for the pragma. Emit an error if this - -- is not the case. - - -------------------- - -- Check_Policies -- - -------------------- - - procedure Check_Policies is - begin - -- If the Ghost policy in effect at the point of the - -- declaration of Ghost entity Id is Ignore, then the assertion - -- policy of the pragma must be Ignore (SPARK RM 6.9(20)). - - if Present (Id) - and then not Is_Checked_Ghost_Entity (Id) - and then not Is_Ignored (Prag) - then - Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref); - Error_Msg_NE - ("\ghost entity & has policy `Ignore`", - Ghost_Ref, Ghost_Id); - Error_Msg_N - ("\assertion expression has policy `Check`", - Ghost_Ref); - end if; - end Check_Policies; - - -- Local variables - Prag_Id : Pragma_Id; Prag_Nam : Name_Id; - -- Start of processing for Is_OK_Pragma - begin if Nkind (Prag) /= N_Pragma then return False; @@ -493,10 +459,6 @@ package body Ghost is and then Assertion_Expression_Pragma (Prag_Id) and then Prag_Id /= Pragma_Predicate then - -- Ensure that the assertion policy and the Ghost policy are - -- compatible (SPARK RM 6.9(20)). - - Check_Policies; return True; -- A pragma that applies to a Ghost construct or specifies an @@ -781,7 +743,7 @@ package body Ghost is elsif Is_OK_Declaration (Par) then return True; - elsif Is_OK_Pragma (Par, Ghost_Id) then + elsif Is_OK_Pragma (Par) then return True; elsif Is_OK_Statement (Par, Ghost_Id, Prev) then
