https://gcc.gnu.org/g:e7368d76b9f41e054204ed42096de165cb9e19f2

commit r17-747-ge7368d76b9f41e054204ed42096de165cb9e19f2
Author: Claire Dross <[email protected]>
Date:   Fri Jan 16 17:02:50 2026 +0100

    ada: Reject exceptional contracts on No_Raise subprograms
    
    Rejectd the SPARK-specific exceptional contract pragmas Exceptional_Cases 
and
    Exit_Cases when they are not compatible with the No_Raise GNAT-specific 
aspect.
    
    gcc/ada/ChangeLog:
    
            * sem_prag.adb (Analyze_Exit_Contract): The Exception_Raised exit 
kind
            is not compatible with No_Raise.
            (Analyze_Pragma): The Exceptional_Cases pragma is not compatible 
with
            No_Raise.

Diff:
---
 gcc/ada/sem_prag.adb | 31 ++++++++++++++++++++++++++++---
 1 file changed, 28 insertions(+), 3 deletions(-)

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 14f49640240d..58d419532226 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2777,9 +2777,15 @@ package body Sem_Prag is
             --  identifiers Normal_Return, Exception_Raised, or Program_Exit.
 
             if Nkind (Exit_Kind) = N_Identifier then
-               if Chars (Exit_Kind) not in Name_Normal_Return
-                                         | Name_Exception_Raised
-                                         | Name_Program_Exit
+               if Chars (Exit_Kind) = Name_Exception_Raised then
+                  if No_Raise (Spec_Id) then
+                     Error_Msg_N
+                       ("exit kind cannot be Exception_Raised on No_Raise " &
+                          "subprogram",
+                        Exit_Kind);
+                  end if;
+               elsif Chars (Exit_Kind) not in Name_Normal_Return
+                                            | Name_Program_Exit
                then
                   Error_Msg_N
                     ("exit kind should be Normal_Return, Exception_Raised, " &
@@ -2812,6 +2818,12 @@ package body Sem_Prag is
                         & "Exception_Raised",
                         Exit_Kind);
 
+                  elsif No_Raise (Spec_Id) then
+                     Error_Msg_N
+                       ("exit kind cannot be Exception_Raised on No_Raise " &
+                          "subprogram",
+                        Exit_Kind);
+
                   elsif Nkind (Exc) /= N_Identifier then
                      Error_Msg_N
                        ("exception name expected after Exception_Raised",
@@ -18218,6 +18230,17 @@ package body Sem_Prag is
                end if;
             end if;
 
+            --  Pragma Exceptional_Cases is not allowed when No_Raise is
+            --  specified.
+
+            Analyze_If_Present (Pragma_No_Raise);
+
+            if No_Raise (Spec_Id) then
+               Error_Msg_N (Fix_Error
+                 ("pragma % cannot apply to No_Raise subprogram"), N);
+               return;
+            end if;
+
             --  A pragma that applies to a Ghost entity becomes Ghost for the
             --  purposes of legality checks and removal of ignored Ghost code.
 
@@ -18404,6 +18427,8 @@ package body Sem_Prag is
 
                Analyze_If_Present (Pragma_SPARK_Mode);
                Analyze_If_Present (Pragma_Volatile_Function);
+               Analyze_If_Present (Pragma_No_Raise);
+
                Analyze_Exit_Cases_In_Decl_Part (N);
             end if;
          end Exit_Cases;

Reply via email to