sem_util.adb (New_Copy_Tree): Code cleanup: removal of the internal map (ie.

2017-01-23  Javier Miranda  <miranda@adacore.com>

	* sem_util.adb (New_Copy_Tree): Code cleanup:
	removal of the internal map (ie. variable Actual_Map, its
	associated local variables, and all the code handling it).
	* sem_ch9.adb (Analyze_Task_Type_Declaration): in GNATprove mode
	force loading of the System package when processing a task type.
	(Analyze_Protected_Type_Declaration): in GNATprove mode force
	loading of the System package when processing a protected type.
	* sem_ch10.adb (Analyze_Compilation_Unit): in GNATprove mode
	force loading of the System package when processing compilation
	unit with a main-like subprogram.
	* frontend.adb (Frontend): remove forced loading of the System
	package.

From-SVN: r244810

gcc/ada/ChangeLog

+2017-01-23  Javier Miranda  <miranda@adacore.com>
+
+	* sem_util.adb (New_Copy_Tree): Code cleanup:
+	removal of the internal map (ie. variable Actual_Map, its
+	associated local variables, and all the code handling it).
+	* sem_ch9.adb (Analyze_Task_Type_Declaration): in GNATprove mode
+	force loading of the System package when processing a task type.
+	(Analyze_Protected_Type_Declaration): in GNATprove mode force
+	loading of the System package when processing a protected type.
+	* sem_ch10.adb (Analyze_Compilation_Unit): in GNATprove mode
+	force loading of the System package when processing compilation
+	unit with a main-like subprogram.
+	* frontend.adb (Frontend): remove forced loading of the System
+	package.
+
 2017-01-23  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_prag.adb (Default_Initial_Condition): If the desired type

gcc/ada/frontend.adb

@@ -463,23 +463,6 @@ begin
       end if;
    end if;
 
-   --  In GNATprove mode, force the loading of a few RTE units. This step is
-   --  skipped if we had a fatal error during parsing.
-
-   if GNATprove_Mode
-     and then Fatal_Error (Main_Unit) /= Error_Detected
-   then
-      declare
-         Unused : Entity_Id;
-
-      begin
-         --  Ensure that System.Interrupt_Priority is available to GNATprove
-         --  for the generation of VCs related to ceiling priority.
-
-         Unused := RTE (RE_Interrupt_Priority);
-      end;
-   end if;
-
    --  Qualify all entity names in inner packages, package bodies, etc
 
    Exp_Dbug.Qualify_All_Entity_Names;

gcc/ada/sem_ch10.adb

@@ -1133,6 +1133,48 @@ package body Sem_Ch10 is
 
             Style_Check := Save_Style_Check;
          end;
+
+         --  In GNATprove mode, force the loading of a Interrupt_Priority when
+         --  processing compilation units with potentially "main" subprograms.
+         --  This is required for the ceiling priority protocol checks, which
+         --  are trigerred by these subprograms.
+
+         if GNATprove_Mode
+           and then Nkind_In (Unit_Node, N_Subprogram_Body,
+                                         N_Procedure_Instantiation,
+                                         N_Function_Instantiation)
+         then
+            declare
+               Spec   : Node_Id;
+               Unused : Entity_Id;
+
+            begin
+               case Nkind (Unit_Node) is
+                  when N_Subprogram_Body =>
+                     Spec := Specification (Unit_Node);
+
+                  when N_Subprogram_Instantiation =>
+                     Spec :=
+                       Subprogram_Specification (Entity (Name (Unit_Node)));
+
+                  when others =>
+                     raise Program_Error;
+               end case;
+
+               pragma Assert (Nkind (Spec) in N_Subprogram_Specification);
+
+               --  Only subprogram with no parameters can act as "main", and if
+               --  it is a function, it needs to return an integer.
+
+               if No (Parameter_Specifications (Spec))
+                 and then (Nkind (Spec) = N_Procedure_Specification
+                             or else
+                           Is_Integer_Type (Etype (Result_Definition (Spec))))
+               then
+                  Unused := RTE (RE_Interrupt_Priority);
+               end if;
+            end;
+         end if;
       end if;
 
       --  Deal with creating elaboration counter if needed. We create an

gcc/ada/sem_ch9.adb

@@ -2257,6 +2257,19 @@ package body Sem_Ch9 is
             Process_Full_View (N, T, Def_Id);
          end if;
       end if;
+
+      --  In GNATprove mode, force the loading of a Interrupt_Priority, which
+      --  is required for the ceiling priority protocol checks trigerred by
+      --  calls originating from protected subprograms and entries.
+
+      if GNATprove_Mode then
+         declare
+            Unused : Entity_Id;
+
+         begin
+            Unused := RTE (RE_Interrupt_Priority);
+         end;
+      end if;
    end Analyze_Protected_Type_Declaration;
 
    ---------------------
@@ -3196,6 +3209,19 @@ package body Sem_Ch9 is
             Process_Full_View (N, T, Def_Id);
          end if;
       end if;
+
+      --  In GNATprove mode, force the loading of a Interrupt_Priority, which
+      --  is required for the ceiling priority protocol checks trigerred by
+      --  calls originating from tasks.
+
+      if GNATprove_Mode then
+         declare
+            Unused : Entity_Id;
+
+         begin
+            Unused := RTE (RE_Interrupt_Priority);
+         end;
+      end if;
    end Analyze_Task_Type_Declaration;
 
    -----------------------------------