blob: d07c351654e31152ba35720c2da33f386de62415 [file] [log] [blame]
-- { dg-do compile }
-- { dg-options "-gnatws" }
package body Synchronized1
with SPARK_Mode,
Refined_State => (State => Curr_State)
is
type Reactor_State is (Stopped, Working) with Atomic;
Curr_State : Reactor_State
with Async_Readers, Async_Writers;
procedure Force_Body is null;
end Synchronized1;