]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
ada: Accept duplicate SPARK_Mode pragmas in configuration files
authorPiotr Trojanek <trojanek@adacore.com>
Tue, 2 Jul 2024 13:19:41 +0000 (15:19 +0200)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Thu, 1 Aug 2024 15:14:38 +0000 (17:14 +0200)
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.

gcc/ada/sem_prag.adb

index 52d63cf44922abcf4458b3f1a946650dff3ea48f..e41fb2f8618abba079f423f14da4ae2440a66037 100644 (file)
@@ -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