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