gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-07/external_test.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
with System.Storage_Elements;
package body External_Test
   with Spark_Mode => On
is

   Value : Byte
     with
       Volatile,
       Async_Readers,
       Effective_Writes,
       Address => System.Storage_Elements.To_Address(16#FFFF0000#);


   procedure Test (Item : out Byte) is
   begin
      Item := Value;
      Item := Value;

      Value := 5;
      Value := 17;

   end Test;

end External_Test;