The test for library units was wrong, resulting in run-time library units being incorrectly marked with SPARK_Mode on when a configuration pragma file had pragma SPARK_Mode (ON).
The following program 1. with Ada.Text_IO; use Ada.Text_IO; 2. procedure SPragLib is 3. begin 4. Put_Line ("Hello World!"); 5. end SPragLib; compiled with -gnatdtf should yield a file that has only one reference to the SPARK_Mode field, not dozens as before. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-01-24 Robert Dewar <de...@adacore.com> * sem.adb (Sem): Avoid premature reference to Current_Sem_Unit (this was causing Is_Main_Unit_Or_Main_Unit_Spec to be set wrong, leading to wrong handling of SPARK_Mode for library units).
Index: sem.adb =================================================================== --- sem.adb (revision 207026) +++ sem.adb (working copy) @@ -1312,18 +1312,19 @@ S_Outer_Gen_Scope : constant Entity_Id := Outer_Generic_Scope; S_Style_Check : constant Boolean := Style_Check; + Curunit : constant Unit_Number_Type := Get_Cunit_Unit_Number (Comp_Unit); + -- New value of Current_Sem_Unit + Generic_Main : constant Boolean := - Nkind (Unit (Cunit (Main_Unit))) - in N_Generic_Declaration; + Nkind (Unit (Cunit (Main_Unit))) in N_Generic_Declaration; -- If the main unit is generic, every compiled unit, including its -- context, is compiled with expansion disabled. Is_Main_Unit_Or_Main_Unit_Spec : constant Boolean := - Current_Sem_Unit = Main_Unit + Curunit = Main_Unit or else (Nkind (Unit (Cunit (Main_Unit))) = N_Package_Body - and then Library_Unit (Cunit (Main_Unit)) = - Cunit (Current_Sem_Unit)); + and then Library_Unit (Cunit (Main_Unit)) = Cunit (Curunit)); -- Configuration flags have special settings when compiling a predefined -- file as a main unit. This applies to its spec as well. @@ -1393,7 +1394,7 @@ end if; Compiler_State := Analyzing; - Current_Sem_Unit := Get_Cunit_Unit_Number (Comp_Unit); + Current_Sem_Unit := Curunit; -- Compile predefined units with GNAT_Mode set to True, to properly -- process the categorization stuff. However, do not set GNAT_Mode