aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2020-09-28 17:58:31 +0200
committerPierre-Marie de Rodat <derodat@adacore.com>2020-11-24 05:15:59 -0500
commit41273281cef411c75d12f45e8083faff2633e61a (patch)
tree8a193228463997f1dfe224a8242d1a7dca8c969a
parent9cfd2c38f39cc2160d057dcd9e44acf73fec58bd (diff)
downloadgcc-41273281cef411c75d12f45e8083faff2633e61a.zip
gcc-41273281cef411c75d12f45e8083faff2633e61a.tar.gz
gcc-41273281cef411c75d12f45e8083faff2633e61a.tar.bz2
[Ada] Reject Global/Depends contracts on null procedures
gcc/ada/ * sem_prag.adb (Analyze_Depends_Global): Reject Global and Depends on null procedure.
-rw-r--r--gcc/ada/sem_prag.adb12
1 files changed, 11 insertions, 1 deletions
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 1e1a279..c64bf48 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