[Ada] Spurious runtime failure on Default_Initial_Condition

[Arnaud Charlet]

This patch ensures that the expression of pragma Default_Initial_Condition is
verified against an object with default initialization.

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

--  dic_pack.ads

generic
   type Element_Typ is private;
   No_Element : Element_Typ;

package DIC_Pack is
   type List (Capacity : Positive) is private
     with Default_Initial_Condition => Is_Empty (List);

   procedure Add (L : in out List; Index : Positive; Val : Element_Typ);
   function Copy (L : List) return List;
   function Is_Empty (L : List) return Boolean;

private
   type Element_Array is array (Positive range <>) of Element_Typ;

   type List (Capacity : Positive) is record
      Data : Element_Array (1 .. Capacity) := (others => No_Element);
   end record;
end DIC_Pack;

--  dic_pack.adb

package body DIC_Pack is
   procedure Add (L : in out List; Index : Positive; Val : Element_Typ) is
   begin
      L.Data (Index) := Val;
   end Add;

   function Copy (L : List) return List is
      Result : List (L.Data'Last);

   begin
      for Index in L.Data'Range loop
         Result.Data (Index) := L.Data (Index);
      end loop;

      return Result;
   end Copy;

   function Is_Empty (L : List) return Boolean is
   begin
      for Index in L.Data'Range loop
         if L.Data (Index) /= No_Element then
            return False;
         end if;
      end loop;

      return True;
   end Is_Empty;
end DIC_Pack;

--  dic_main.adb

with DIC_Pack;

procedure DIC_Main is
   package DIC_Inst is new DIC_Pack (Element_Typ => Integer, No_Element => 0);

   L1 : DIC_Inst.List (5);
   L2 : DIC_Inst.List (5) := DIC_Inst.Copy (L1);

begin
   DIC_Inst.Add (L1, 2, 4);

   declare
      L2 : DIC_Inst.List (5) := DIC_Inst.Copy (L1);
   begin
      null;
   end;
end DIC_Main;

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

$ gnatmake -q -gnata dic_main.adb
$ ./dic_main

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

2015-03-04  Hristian Kirtchev  <kirtc...@adacore.com>

        * exp_ch3.adb (Expand_N_Object_Declaration):
        Generate a runtime check to test the expression of pragma
        Default_Initial_Condition when the object is default initialized.


Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb (revision 221175)
+++ exp_ch3.adb (working copy)
@@ -6138,11 +6138,9 @@
          end;
       end if;
 
-      --  At this point the object is fully initialized by either invoking the
-      --  related type init proc, routine [Deep_]Initialize or performing in-
-      --  place assingments for an array object. If the related type is subject
-      --  to pragma Default_Initial_Condition, add a runtime check to verify
-      --  the assumption of the pragma. Generate:
+      --  If the object is default initialized and its type is subject to
+      --  pragma Default_Initial_Condition, add a runtime check to verify
+      --  the assumption of the pragma (SPARK RM 7.3.3). Generate:
 
       --    <Base_Typ>Default_Init_Cond (<Base_Typ> (Def_Id));
 
@@ -6152,6 +6150,7 @@
         and then (Has_Default_Init_Cond           (Base_Typ)
                     or else
                   Has_Inherited_Default_Init_Cond (Base_Typ))
+        and then not Has_Init_Expression (N)
       then
          declare
             DIC_Call : constant Node_Id :=