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

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

package Trivial_Effective_Properties
  with SPARK_Mode
is

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

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

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

end Trivial_Effective_Properties;