https://gcc.gnu.org/g:aced54ff681f671b2c5b99d18dddbbc570ac2a57
commit r15-2634-gaced54ff681f671b2c5b99d18dddbbc570ac2a57
Author: Piotr Trojanek <troja...@adacore.com>
Date: Tue Jul 2 15:19:41 2024 +0200
ada: Accept duplicate SPARK_Mode pragmas in configuration files
For consistency, we now accept duplicate SPARK_Mode pragmas in
configuration files just like we accept other duplicate pragas there.
gcc/ada/
* sem_prag.adb (Analyze_Pragma): Don't check for duplicate
SPARK_Mode pragmas in configuration files.
Diff:
---
gcc/ada/sem_prag.adb | 8 --------
1 file changed, 8 deletions(-)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 52d63cf44922..e41fb2f8618a 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -24758,14 +24758,6 @@ package body Sem_Prag is
if No (Context) then
Check_Valid_Configuration_Pragma;
-
- if Present (SPARK_Mode_Pragma) then
- Duplication_Error
- (Prag => N,
- Prev => SPARK_Mode_Pragma);
- raise Pragma_Exit;
- end if;
-
Set_SPARK_Context;
-- The pragma acts as a configuration pragma in a compilation unit
