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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
with System.Storage_Elements;

package body Indicator
  with Refined_State => (Outputs => Output_Ext)
is
   type Settings is new Boolean;

   Output_Ext : Settings
     with Volatile,
          Async_Readers,
          Address => System.Storage_Elements.To_Address (16#FFFF_FFFF#);

   procedure TurnOn
     with Refined_Global  => (Output => Output_Ext),
          Refined_Depends => (Output_Ext => null)
   is
   begin
      Output_Ext := True;
   end TurnOn;

   procedure TurnOff
     with Refined_Global  => (Output => Output_Ext),
          Refined_Depends => (Output_Ext => null)
   is
   begin
      Output_Ext := False;
   end TurnOff;

end Indicator;