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