[multiple changes]

2017-04-25  Arnaud Charlet  <charlet@adacore.com>

	* rtsfind.ads (SPARK_Implicit_Load): New procedure for forced
	loading of an entity.
	* rtsfind.adb (SPARK_Implicit_Load): Body with a pattern
	previously repeated in the analysis.
	* sem_ch9.adb (Analyze_Protected_Type_Declaration): use new
	procedure SPARK_Implicit_Load.	(Analyze_Task_Type_Declaration):
	use new procedure SPARK_Implicit_Load.
	* sem_ch10.adb (Analyze_Compilation_Unit): Use new procedure
	SPARK_Implicit_Load.

2017-04-25  Javier Miranda  <miranda@adacore.com>

	* sem_util.adb (New_Copy_Tree): By default
	copying of defining identifiers is prohibited because
	this would introduce an entirely new entity into the
	tree. This patch introduces an exception to this general
	rule: the declaration of constants and variables located in
	Expression_With_Action nodes.
	(Copy_Itype_With_Replacement): Renamed as Copy_Entity_With_Replacement.
	(In_Map): New subprogram.
	(Visit_Entity): New subprogram.
	(Visit_Node): Handle EWA_Level,
	EWA_Inner_Scope_Level, and take care of defining entities defined
	in Expression_With_Action nodes.

2017-04-25  Thomas Quinot  <quinot@adacore.com>

	* exp_ch6.adb: minor comment edit.
	* sinfo.ads, sinfo.adb: New Null_Statement attribute for null
	procedure specifications that come from source.
	* par-ch6.adb (P_Subprogram, case of a null procedure): Set new
	Null_Statement attribute.
	* par_sco.adb (Traverse_Declarations_Or_Statements): For a null
	procedure, generate statement SCO for the generated NULL statement.
	* sem_ch6.adb (Analyze_Null_Procedure): Use null statement from
	parser, if available.

From-SVN: r247136

gcc/ada/ChangeLog

+2017-04-25  Arnaud Charlet  <charlet@adacore.com>
+
+	* rtsfind.ads (SPARK_Implicit_Load): New procedure for forced
+	loading of an entity.
+	* rtsfind.adb (SPARK_Implicit_Load): Body with a pattern
+	previously repeated in the analysis.
+	* sem_ch9.adb (Analyze_Protected_Type_Declaration): use new
+	procedure SPARK_Implicit_Load.	(Analyze_Task_Type_Declaration):
+	use new procedure SPARK_Implicit_Load.
+	* sem_ch10.adb (Analyze_Compilation_Unit): Use new procedure
+	SPARK_Implicit_Load.
+
+2017-04-25  Javier Miranda  <miranda@adacore.com>
+
+	* sem_util.adb (New_Copy_Tree): By default
+	copying of defining identifiers is prohibited because
+	this would introduce an entirely new entity into the
+	tree. This patch introduces an exception to this general
+	rule: the declaration of constants and variables located in
+	Expression_With_Action nodes.
+	(Copy_Itype_With_Replacement): Renamed as Copy_Entity_With_Replacement.
+	(In_Map): New subprogram.
+	(Visit_Entity): New subprogram.
+	(Visit_Node): Handle EWA_Level,
+	EWA_Inner_Scope_Level, and take care of defining entities defined
+	in Expression_With_Action nodes.
+
+2017-04-25  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_ch6.adb: minor comment edit.
+	* sinfo.ads, sinfo.adb: New Null_Statement attribute for null
+	procedure specifications that come from source.
+	* par-ch6.adb (P_Subprogram, case of a null procedure): Set new
+	Null_Statement attribute.
+	* par_sco.adb (Traverse_Declarations_Or_Statements): For a null
+	procedure, generate statement SCO for the generated NULL statement.
+	* sem_ch6.adb (Analyze_Null_Procedure): Use null statement from
+	parser, if available.
+
 2017-04-04  Andreas Krebbel  <krebbel@linux.vnet.ibm.com>
 
 	* system-linux-s390.ads: Use Long_Integer'Size to define

gcc/ada/exp_ch6.adb

@@ -5763,7 +5763,7 @@ package body Exp_Ch6 is
       --  Ada 2005 (AI-348): Generate body for a null procedure. In most
       --  cases this is superfluous because calls to it will be automatically
       --  inlined, but we definitely need the body if preconditions for the
-      --  procedure are present.
+      --  procedure are present, or if performing coverage analysis.
 
       elsif Nkind (Specification (N)) = N_Procedure_Specification
         and then Null_Present (Specification (N))

gcc/ada/par-ch6.adb

@@ -607,6 +607,8 @@ package body Ch6 is
                   Error_Msg_SP ("only procedures can be null");
                else
                   Set_Null_Present (Specification_Node);
+                  Set_Null_Statement (Specification_Node,
+                    New_Node (N_Null_Statement, Prev_Token_Ptr));
                end if;
 
                goto Subprogram_Declaration;

gcc/ada/par_sco.adb

@@ -1812,13 +1812,15 @@ package body Par_SCO is
                   Process_Decisions_Defer
                     (Parameter_Specifications (Spec), 'X');
 
-                  --  Case of a null procedure: generate a NULL statement SCO
+                  --  Case of a null procedure: generate SCO for fictitious
+                  --  NULL statement located at the NULL keyword in the
+                  --  procedure specification.
 
                   if Nkind (N) = N_Subprogram_Declaration
                     and then Nkind (Spec) = N_Procedure_Specification
                     and then Null_Present (Spec)
                   then
-                     Traverse_Degenerate_Subprogram (N);
+                     Traverse_Degenerate_Subprogram (Null_Statement (Spec));
 
                   --  Case of an expression function: generate a statement SCO
                   --  for the expression (and then decision SCOs for any nested

gcc/ada/rtsfind.adb

@@ -1646,4 +1646,18 @@ package body Rtsfind is
       end loop;
    end Set_RTU_Loaded;
 
+   -------------------------
+   -- SPARK_Implicit_Load --
+   -------------------------
+
+   procedure SPARK_Implicit_Load (E : RE_Id) is
+      Unused : Entity_Id;
+
+   begin
+      pragma Assert (GNATprove_Mode);
+
+      --  Force loading of a predefined unit
+      Unused := RTE (E);
+   end SPARK_Implicit_Load;
+
 end Rtsfind;

gcc/ada/rtsfind.ads

@@ -3223,4 +3223,9 @@ package Rtsfind is
    procedure Set_RTU_Loaded (N : Node_Id);
    --  Register the predefined unit N as already loaded
 
+   procedure SPARK_Implicit_Load (E : RE_Id);
+   --  Force loading of the unit containing the entity E; only needed in
+   --  GNATprove mode when processing code that implicitly references a
+   --  given entity.
+
 end Rtsfind;

gcc/ada/sem_ch10.adb

@@ -1145,8 +1145,7 @@ package body Sem_Ch10 is
                                          N_Function_Instantiation)
          then
             declare
-               Spec   : Node_Id;
-               Unused : Entity_Id;
+               Spec : Node_Id;
 
             begin
                case Nkind (Unit_Node) is
@@ -1163,15 +1162,15 @@ package body Sem_Ch10 is
 
                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.
+               --  Main subprogram must have no parameters, and if it is a
+               --  function, it must 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);
+                  SPARK_Implicit_Load (RE_Interrupt_Priority);
                end if;
             end;
          end if;

gcc/ada/sem_ch6.adb

@@ -1370,6 +1370,7 @@ package body Sem_Ch6 is
       Designator : Entity_Id;
       Form       : Node_Id;
       Null_Body  : Node_Id := Empty;
+      Null_Stmt  : Node_Id := Null_Statement (Spec);
       Prev       : Entity_Id;
 
    begin
@@ -1379,13 +1380,22 @@ package body Sem_Ch6 is
       --  the first case the body is analyzed at the freeze point, in the other
       --  it replaces the null procedure declaration.
 
+      --  For a null procedure that comes from source, a NULL statement is
+      --  provided by the parser, which carries the source location of the
+      --  NULL keyword, and has Comes_From_Source set. For a null procedure
+      --  from expansion, create one now.
+
+      if No (Null_Stmt) then
+         Null_Stmt := Make_Null_Statement (Loc);
+      end if;
+
       Null_Body :=
         Make_Subprogram_Body (Loc,
           Specification => New_Copy_Tree (Spec),
           Declarations  => New_List,
           Handled_Statement_Sequence =>
             Make_Handled_Sequence_Of_Statements (Loc,
-              Statements => New_List (Make_Null_Statement (Loc))));
+              Statements => New_List (Null_Stmt)));
 
       --  Create new entities for body and formals
 

gcc/ada/sem_ch9.adb

@@ -1169,12 +1169,7 @@ package body Sem_Ch9 is
       --  force the loading of the Ada.Real_Time package.
 
       if GNATprove_Mode then
-         declare
-            Unused : Entity_Id;
-
-         begin
-            Unused := RTE (RO_RT_Time);
-         end;
+         SPARK_Implicit_Load (RO_RT_Time);
       end if;
    end Analyze_Delay_Relative;
 
@@ -2263,12 +2258,7 @@ package body Sem_Ch9 is
       --  calls originating from protected subprograms and entries.
 
       if GNATprove_Mode then
-         declare
-            Unused : Entity_Id;
-
-         begin
-            Unused := RTE (RE_Interrupt_Priority);
-         end;
+         SPARK_Implicit_Load (RE_Interrupt_Priority);
       end if;
    end Analyze_Protected_Type_Declaration;
 
@@ -3215,12 +3205,7 @@ package body Sem_Ch9 is
       --  calls originating from tasks.
 
       if GNATprove_Mode then
-         declare
-            Unused : Entity_Id;
-
-         begin
-            Unused := RTE (RE_Interrupt_Priority);
-         end;
+         SPARK_Implicit_Load (RE_Interrupt_Priority);
       end if;
    end Analyze_Task_Type_Declaration;
 

gcc/ada/sinfo.adb

@@ -2472,16 +2472,6 @@ package body Sinfo is
       return Flag18 (N);
    end Non_Aliased_Prefix;
 
-   function Null_Present
-      (N : Node_Id) return Boolean is
-   begin
-      pragma Assert (False
-        or else NT (N).Nkind = N_Component_List
-        or else NT (N).Nkind = N_Procedure_Specification
-        or else NT (N).Nkind = N_Record_Definition);
-      return Flag13 (N);
-   end Null_Present;
-
    function Null_Excluding_Subtype
       (N : Node_Id) return Boolean is
    begin
@@ -2519,6 +2509,16 @@ package body Sinfo is
       return Flag14 (N);
    end Null_Exclusion_In_Return_Present;
 
+   function Null_Present
+      (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Component_List
+        or else NT (N).Nkind = N_Procedure_Specification
+        or else NT (N).Nkind = N_Record_Definition);
+      return Flag13 (N);
+   end Null_Present;
+
    function Null_Record_Present
       (N : Node_Id) return Boolean is
    begin
@@ -2528,6 +2528,14 @@ package body Sinfo is
       return Flag17 (N);
    end Null_Record_Present;
 
+   function Null_Statement
+      (N : Node_Id) return Node_Id is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Procedure_Specification);
+      return Node2 (N);
+   end Null_Statement;
+
    function Object_Definition
       (N : Node_Id) return Node_Id is
    begin
@@ -5774,16 +5782,6 @@ package body Sinfo is
       Set_Flag18 (N, Val);
    end Set_Non_Aliased_Prefix;
 
-   procedure Set_Null_Present
-      (N : Node_Id; Val : Boolean := True) is
-   begin
-      pragma Assert (False
-        or else NT (N).Nkind = N_Component_List
-        or else NT (N).Nkind = N_Procedure_Specification
-        or else NT (N).Nkind = N_Record_Definition);
-      Set_Flag13 (N, Val);
-   end Set_Null_Present;
-
    procedure Set_Null_Excluding_Subtype
       (N : Node_Id; Val : Boolean := True) is
    begin
@@ -5821,6 +5819,16 @@ package body Sinfo is
       Set_Flag14 (N, Val);
    end Set_Null_Exclusion_In_Return_Present;
 
+   procedure Set_Null_Present
+      (N : Node_Id; Val : Boolean := True) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Component_List
+        or else NT (N).Nkind = N_Procedure_Specification
+        or else NT (N).Nkind = N_Record_Definition);
+      Set_Flag13 (N, Val);
+   end Set_Null_Present;
+
    procedure Set_Null_Record_Present
       (N : Node_Id; Val : Boolean := True) is
    begin
@@ -5830,6 +5838,14 @@ package body Sinfo is
       Set_Flag17 (N, Val);
    end Set_Null_Record_Present;
 
+   procedure Set_Null_Statement
+      (N : Node_Id; Val : Node_Id) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Procedure_Specification);
+      Set_Node2 (N, Val);
+   end Set_Null_Statement;
+
    procedure Set_Object_Definition
       (N : Node_Id; Val : Node_Id) is
    begin

gcc/ada/sinfo.ads

@@ -5155,6 +5155,7 @@ package Sinfo is
       --  N_Procedure_Specification
       --  Sloc points to PROCEDURE
       --  Defining_Unit_Name (Node1)
+      --  Null_Statement (Node2-Sem) NULL statement for body, if Null_Present
       --  Parameter_Specifications (List3) (set to No_List if no formal part)
       --  Generic_Parent (Node5-Sem)
       --  Null_Present (Flag13) set for null procedure case (Ada 2005 feature)
@@ -9699,9 +9700,6 @@ package Sinfo is
    function Non_Aliased_Prefix
      (N : Node_Id) return Boolean;    -- Flag18
 
-   function Null_Present
-     (N : Node_Id) return Boolean;    -- Flag13
-
    function Null_Excluding_Subtype
      (N : Node_Id) return Boolean;    -- Flag16
 
@@ -9711,9 +9709,15 @@ package Sinfo is
    function Null_Exclusion_In_Return_Present
      (N : Node_Id) return Boolean;    -- Flag14
 
+   function Null_Present
+     (N : Node_Id) return Boolean;    -- Flag13
+
    function Null_Record_Present
      (N : Node_Id) return Boolean;    -- Flag17
 
+   function Null_Statement
+     (N : Node_Id) return Node_Id;    -- Node2
+
    function Object_Definition
      (N : Node_Id) return Node_Id;    -- Node4
 
@@ -10755,9 +10759,6 @@ package Sinfo is
    procedure Set_Non_Aliased_Prefix
      (N : Node_Id; Val : Boolean := True);    -- Flag18
 
-   procedure Set_Null_Present
-     (N : Node_Id; Val : Boolean := True);    -- Flag13
-
    procedure Set_Null_Excluding_Subtype
      (N : Node_Id; Val : Boolean := True);    -- Flag16
 
@@ -10767,9 +10768,15 @@ package Sinfo is
    procedure Set_Null_Exclusion_In_Return_Present
      (N : Node_Id; Val : Boolean := True);    -- Flag14
 
+   procedure Set_Null_Present
+     (N : Node_Id; Val : Boolean := True);    -- Flag13
+
    procedure Set_Null_Record_Present
      (N : Node_Id; Val : Boolean := True);    -- Flag17
 
+   procedure Set_Null_Statement
+     (N : Node_Id; Val : Node_Id);            -- Node2
+
    procedure Set_Object_Definition
      (N : Node_Id; Val : Node_Id);            -- Node4
 
@@ -11900,7 +11907,7 @@ package Sinfo is
 
      N_Procedure_Specification =>
        (1 => True,    --  Defining_Unit_Name (Node1)
-        2 => False,   --  unused
+        2 => False,   --  Null_Statement (Node2-Sem)
         3 => True,    --  Parameter_Specifications (List3)
         4 => False,   --  unused
         5 => False),  --  Generic_Parent (Node5-Sem)
@@ -13088,11 +13095,12 @@ package Sinfo is
    pragma Inline (No_Side_Effect_Removal);
    pragma Inline (No_Truncation);
    pragma Inline (Non_Aliased_Prefix);
-   pragma Inline (Null_Present);
    pragma Inline (Null_Excluding_Subtype);
    pragma Inline (Null_Exclusion_Present);
    pragma Inline (Null_Exclusion_In_Return_Present);
+   pragma Inline (Null_Present);
    pragma Inline (Null_Record_Present);
+   pragma Inline (Null_Statement);
    pragma Inline (Object_Definition);
    pragma Inline (Of_Present);
    pragma Inline (Original_Discriminant);
@@ -13441,6 +13449,7 @@ package Sinfo is
    pragma Inline (Set_Null_Exclusion_In_Return_Present);
    pragma Inline (Set_Null_Present);
    pragma Inline (Set_Null_Record_Present);
+   pragma Inline (Set_Null_Statement);
    pragma Inline (Set_Object_Definition);
    pragma Inline (Set_Of_Present);
    pragma Inline (Set_Original_Discriminant);