Type_Invariant and instance creation (was: Type_Invariant and Finalize)

[Simon Wright <simon@pushface.org>]

I wrote this to play with some of the concepts Natasha discussed, since
I haven't used the contract aspects before. It's a bit more complicated
than I'd have hoped because of the need for Adjust.

As it stands, it executes as expected with GNAT GPL 2014 (that is, the
finalizations occur OK and don't trigger assertion failures, but the
creation of an empty object does).

With FSF GCC 4.9.0, however, the assertion fails in Create at

      return (Ada.Finalization.Controlled with V => new Integer'(Value));

I tried inserting Put_Lines in the test program to get an idea of the
flow:

   declare
      Tmp : Releasing_Not_Null.R := Releasing_Not_Null.Create (42);
   begin
      Put_Line ("in first declare block");
   end;
   Put_Line ("first declare block done");

and now blow me down if GNAT GPL 2014 doesn't fail just like FSF GCC!

What am I doing wrong? Which compiler (if either) is right?

-- gnatchop from here --
with Ada.Finalization;
package Releasing_Not_Null is
   type R is new Ada.Finalization.Controlled with private;
   function Create (Value : Integer) return R;
private
   type P is access Integer;
   type R is new Ada.Finalization.Controlled with record
      V : P;
   end record
      with Type_Invariant => R.V /= null;
   overriding
   procedure Adjust (This : in out R);
   overriding
   procedure Finalize (This : in out R);
end Releasing_Not_Null;
with Ada.Unchecked_Deallocation;
package body Releasing_Not_Null is
   function Create (Value : Integer) return R is
   begin
      return (Ada.Finalization.Controlled with V => new Integer'(Value));
   end Create;
   procedure Adjust (This : in out R) is
   begin
      This.V := new Integer'(This.V.all);
   end Adjust;
   procedure Finalize (This : in out R) is
      procedure Free is new Ada.Unchecked_Deallocation (Integer, P);
   begin
      if This.V /= null then
         Free (This.V);
      end if;
   end Finalize;
end Releasing_Not_Null;
with Releasing_Not_Null;
procedure Test_Releasing_Not_Null is
begin
   declare  -- this block is OK
      Tmp : Releasing_Not_Null.R := Releasing_Not_Null.Create (42);
   begin
      null;
   end;
   declare
      Tmp : Releasing_Not_Null.R;  -- Failed invariant here
   begin
      null;
   end;
end Test_Releasing_Not_Null;