| -- { 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; |