gnatprove_13.2.1_28fc3583/share/examples/spark/heatingsystem/clock.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
with System.Storage_Elements;

-- Clock
package body Clock
  with Refined_State => (Ticks => Tick_Ext)
is
   Tick_Ext : Times
     with Volatile,
          Async_Writers,
          Address => System.Storage_Elements.To_Address (16#FFFF_FFFF#);

   procedure Read (Time : out Times)
     with Refined_Global  => Tick_Ext,
          Refined_Depends => (Time => Tick_Ext)
   is
   begin
      Time := Tick_Ext;
   end Read;

end Clock;