[Ada] Crash on early call region of SPARK subprogram body

[Pierre-Marie de Rodat]

This patch accounts for the case where the early call region of a subprogram
body declared in a package body spans into the empty corresponding spec due to
pragma Elaborate_Body.

------------
-- Source --
------------

--  gnat.adc

pragma SPARK_Mode (On);

--  pack.ads

package Pack with Elaborate_Body is
end Pack;

--  pack.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Pack is
   procedure Proc;

   procedure Elaborator is
   begin
      Proc;
   end Elaborator;

   procedure Proc is
   begin
      Put_Line ("Proc");
   end Proc;

begin
   Elaborator;
end Pack;

-----------------
-- Compilation --
-----------------

$ gcc -c pack.adb

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-11-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb (Include): Including a node which is also a compilation
	unit terminates the search because there are no more lists to examine.

-------------- next part --------------
Index: sem_elab.adb
===================================================================
--- sem_elab.adb	(revision 254803)
+++ sem_elab.adb	(working copy)
@@ -4245,7 +4245,7 @@
       procedure Include (N : Node_Id; Curr : in out Node_Id);
       pragma Inline (Include);
       --  Update the Curr and Start pointers to include arbitrary construct N
-      --  in the early call region.
+      --  in the early call region. This routine raises ECR_Found.
 
       function Is_OK_Preelaborable_Construct (N : Node_Id) return Boolean;
       pragma Inline (Is_OK_Preelaborable_Construct);
@@ -4559,7 +4559,24 @@
       procedure Include (N : Node_Id; Curr : in out Node_Id) is
       begin
          Start := N;
-         Curr  := Prev (Start);
+
+         --  The input node is a compilation unit. This terminates the search
+         --  because there are no more lists to inspect and there are no more
+         --  enclosing constructs to climb up to. The transitions are:
+         --
+         --    private declarations -> terminate
+         --    visible declarations -> terminate
+         --    statements           -> terminate
+         --    declarations         -> terminate
+
+         if Nkind (Parent (Start)) = N_Compilation_Unit then
+            raise ECR_Found;
+
+         --  Otherwise the input node is still within some list
+
+         else
+            Curr := Prev (Start);
+         end if;
       end Include;
 
       -----------------------------------