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

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

package Trivial
  with SPARK_Mode
is

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

   X : Integer with Volatile, Address => Ext_Address;

   procedure Get (Val : out Integer) with
     Global  => (In_Out => X),
     Depends => (Val => X,
                 X   => X);

end Trivial;