gcc/testsuite/gnat.dg/synchronized1.adb

   1 -- { dg-do compile }
   2 -- { dg-options "-gnatws" }
   3
   4 package body Synchronized1
   5   with SPARK_Mode,
   6        Refined_State => (State => Curr_State)
   7 is
   8    type Reactor_State is (Stopped, Working) with Atomic;
   9
  10    Curr_State : Reactor_State
  11      with Async_Readers, Async_Writers;
  12
  13    procedure Force_Body is null;
  14 end Synchronized1;