From: Yannick Moy <moy@adacore.com>
Date: Mon, 28 Sep 2020 15:58:31 +0000 (+0200)
Subject: [Ada] Reject Global/Depends contracts on null procedures
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41273281cef411c75d12f45e8083faff2633e61a;p=gcc.git

[Ada] Reject Global/Depends contracts on null procedures

gcc/ada/

	* sem_prag.adb (Analyze_Depends_Global): Reject Global and
	Depends on null procedure.
---

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 1e1a279da2e..c64bf48167f 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -4437,7 +4437,17 @@ package body Sem_Prag is
          --  Subprogram declaration
 
          elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
-            null;
+
+            --  Pragmas Global and Depends are forbidden on null procedures
+            --  (SPARK RM 6.1.2(2)).
+
+            if Nkind (Specification (Subp_Decl)) = N_Procedure_Specification
+              and then Null_Present (Specification (Subp_Decl))
+            then
+               Error_Msg_N (Fix_Error
+                 ("pragma % cannot apply to null procedure"), N);
+               return;
+            end if;
 
          --  Task type