The compiler can generate a call to a type's invariant-checking procedure on an uninitialized object, such as a temporary object created for holding an aggregate. This is prevented by inhibiting the call when No_Initialization is set on the object.
The following test must compile and execute quietly with -gnata: package Sat is type T_Sat is abstract tagged private; type T_Sat_Class_Access is access all T_Sat'Class; procedure Compute (Self : in out T_Sat; Time : in Natural; Alt : out Natural) is abstract with Pre'Class => Time <= 7 * 24 * 60 * 60; private type T_Sat is abstract tagged record I : Integer:= 5; end record; -- with type_invariant => T_Sat.I in 1.. 10; end Sat; with Sat; use Sat; package Gps is type T_Gps is new T_Sat with private; type T_Gps_Access is access all T_Gps; package Constructors is function Initialize return T_Gps; end Constructors; overriding procedure Compute (Self : in out T_Gps; Time : in Natural; Alt : out Natural) with Pre'Class => Time <= 7 * 24 * 60 * 60; private type T_Gps is new T_Sat with record J : Integer := 5; end record with Type_Invariant => T_Gps.J in 1 .. 10; end Gps; package body Gps is package body Constructors is function Initialize return T_Gps is begin return T_Gps'(T_Sat with J => 1); end Initialize; end Constructors; procedure Compute (Self : in out T_Gps; Time : in Natural; Alt : out Natural) is pragma Unreferenced (Self, Time); begin Alt := 20_000_000; end Compute; end Gps; with Sat; use Sat; with Gps; use Gps; procedure Main is Un_Autre_Gps : T_Gps; Un_Gps : T_Sat_Class_Access := new T_Gps'(Constructors.Initialize); Alt : Natural; begin Compute (Self => Un_Gps.all, Time => 604800, Alt => Alt); end Main; Tested on x86_64-pc-linux-gnu, committed on trunk 2014-08-04 Gary Dismukes <dismu...@adacore.com> * exp_ch3.adb (Expand_N_Object_Declaration): Inhibit generation of an invariant check in the case where No_Initialization is set, since the object is uninitialized.
Index: exp_ch3.adb =================================================================== --- exp_ch3.adb (revision 213536) +++ exp_ch3.adb (working copy) @@ -5412,11 +5412,14 @@ -- is raised, then the object will go out of scope. In the case where -- an array object is initialized with an aggregate, the expression -- is removed. Check flag Has_Init_Expression to avoid generating a - -- junk invariant check. + -- junk invariant check and flag No_Initialization to avoid checking + -- an uninitialized object such as a compiler temporary used for an + -- aggregate. if Has_Invariants (Base_Typ) and then Present (Invariant_Procedure (Base_Typ)) and then not Has_Init_Expression (N) + and then not No_Initialization (N) then Insert_After (N, Make_Invariant_Call (New_Occurrence_Of (Def_Id, Loc)));