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 :=