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 --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 14f49640240d7d8d8f99bd5516b7cdca078bdbf7..58d419532226f7e7fe9227c3d4b250614de8c1f4 100644 (file)
--- 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;