diff mbox

[Ada] Type invariant procedure called on an uninitialized object

Message ID 20140804095513.GA19756@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 4, 2014, 9:55 a.m. UTC 
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  <dismukes@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.
diff mbox

Patch

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)));