From 41273281cef411c75d12f45e8083faff2633e61a Mon Sep 17 00:00:00 2001
From: Yannick Moy <moy@adacore.com>
Date: Mon, 28 Sep 2020 17:58:31 +0200
Subject: [PATCH] [Ada] Reject Global/Depends contracts on null procedures

gcc/ada/

	* sem_prag.adb (Analyze_Depends_Global): Reject Global and
	Depends on null procedure.
---
 gcc/ada/sem_prag.adb | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

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
 
-- 
2.30.2