1--  { dg-do run }
2--  { dg-options "-gnata" }
3
4procedure 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;
24begin
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;
40end Predicate1;
41