gcc/testsuite/gnat.dg/predicate1.adb

   1 --  { dg-do run }
   2 --  { dg-options "-gnata" }
   3
   4 procedure Predicate1 with SPARK_Mode is
   5     type R is record
   6        F : Integer;
   7     end record;
   8
   9     package Nested is
  10        subtype S is R with Predicate => S.F = 42;
  11        procedure P (X : in out S) is null;
  12
  13        type T is private;
  14        procedure P (X : in out T) is null;
  15     private
  16        type T is new S;
  17     end Nested;
  18
  19     X : Nested.T;
  20     Y : Nested.S;
  21
  22     X_Uninitialized : Boolean := False;
  23     Y_Uninitialized : Boolean := False;
  24 begin
  25    begin
  26       Nested.P (X);
  27    exception
  28       when others => X_Uninitialized := True;
  29    end;
  30
  31    begin
  32       Nested.P (Y);
  33    exception
  34       when others => Y_Uninitialized := True;
  35    end;
  36
  37    if not X_Uninitialized or else not Y_Uninitialized then
  38       raise Program_Error;
  39    end if;
  40 end Predicate1;