gnatprove_13.2.1_28fc3583/share/examples/spark/adacore_u/Systems_Programming/trivial_async_properties.ads

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

package Trivial_Async_Properties
  with SPARK_Mode
is

   Ext_Address : constant System.Address :=
     System.Storage_Elements.To_Address (16#ABCD#);

   X : Integer with Volatile, Address => Ext_Address, Async_Readers;
   Y : Integer with Volatile, Address => Ext_Address, Async_Writers;

   procedure Set with
     Depends => (X    => null,
                 null => Y);

end Trivial_Async_Properties;