gcc/testsuite/gnat.dg/null_check.adb

   1 --  { dg-do run }
   2
   3 procedure Null_Check with SPARK_Mode is
   4    type Int_Ptr is access Integer;
   5    subtype Not_Null_Int_Ptr is not null Int_Ptr;
   6
   7    procedure Set_To_Null (X : out Int_Ptr) with Global => null is
   8    begin
   9       X := null;
  10    end Set_To_Null;
  11
  12    X : Not_Null_Int_Ptr := new Integer'(12);
  13 begin
  14    Set_To_Null (X);
  15    raise Program_Error;
  16 exception
  17    when Constraint_Error =>
  18       null;
  19 end Null_Check;