diff mbox series

[COMMITTED,20/27] ada: Add Assertion_Policy checks for assertion levels

Message ID 20250915130135.2720894-20-poulhies@adacore.com
State Committed
Commit 33f64b23787acff88f0970715342fa8e797016c5
Headers
Series [COMMITTED,01/27] ada: Fix documentation of Is_Ancestor_Package |

Commit Message

Marc Poulhiès Sept. 15, 2025, 1:01 p.m. UTC 
  From: Viljar Indus <indus@adacore.com>

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.

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

---
 gcc/ada/sem_prag.adb | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
diff mbox series

Patch

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);