https://gcc.gnu.org/g:33f64b23787acff88f0970715342fa8e797016c5
commit r16-3879-g33f64b23787acff88f0970715342fa8e797016c5 Author: Viljar Indus <[email protected]> Date: Tue Sep 2 13:11:30 2025 +0300 ada: Add Assertion_Policy checks for assertion levels Implement SPARK RM 6.9(19) check: An Assertion_Policy pragma specifying an Assertion_Level policy shall not occur within a ghost subprogram or package associated to an assertion level which depends on this level. gcc/ada/ChangeLog: * sem_prag.adb (Analyze_Pragma): Add ghost level check to Assertion_Policy. Diff: --- gcc/ada/sem_prag.adb | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 9175490eca27..172dc3d6f3ec 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -14845,6 +14845,22 @@ package body Sem_Prag is ("invalid assertion kind for pragma%", Arg); end if; + + -- An Assertion_Policy pragma specifying an + -- Assertion_Level policy shall not occur within a ghost + -- subprogram or package associated to an assertion level + -- which depends on this level (SPARK RM 6.9(19)). + + if Ghost_Config.Ghost_Mode > None + and then Is_Same_Or_Depends_On_Level + (Ghost_Config.Ghost_Mode_Assertion_Level, + Level) + then + Error_Msg_Name_2 := Chars (Level); + Error_Pragma + ("pragma % cannot appear within ghost subprogram or " + & "package that depends on %"); + end if; end if; Check_Arg_Is_One_Of (Arg, Policy_Names);
