1--  { dg-do compile }
2
3package body Sync2 with
4  SPARK_Mode,
5  Refined_State => (State => (A, P, T))
6is
7   A : Integer := 0 with Atomic, Async_Readers, Async_Writers;
8
9   protected type Prot_Typ is
10   private
11      Comp : Natural := 0;
12   end Prot_Typ;
13
14   P : Prot_Typ;
15
16   task type Task_Typ;
17
18   T : Task_Typ;
19
20   protected body Prot_Typ is
21   end Prot_Typ;
22
23   task body Task_Typ is
24   begin
25      null;
26   end Task_Typ;
27end Sync2;
28