diff mbox series

[COMMITTED,28/30] ada: Accept duplicate SPARK_Mode pragmas in configuration files

Message ID 20240801151738.400796-28-poulhies@adacore.com
State New
Headers show
Series [COMMITTED,01/30] ada: Remove obsolete workaround | expand

Commit Message

Marc Poulhiès Aug. 1, 2024, 3:17 p.m. UTC 
From: Piotr Trojanek <trojanek@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/sem_prag.adb | 8 --------
 1 file changed, 8 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 52d63cf4492..e41fb2f8618 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