gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-07/numeric_display.ads

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
with System.Storage_Elements;
package Numeric_Display
  with SPARK_Mode => On
is
   type Octet is mod 2**8;

   Value : Octet
     with
       Size => 8,  -- Use exactly 8 bits for this variable
       Volatile         => True,
       Async_Readers    => True,
       Effective_Writes => True,
       Address => System.Storage_Elements.To_Address(16#FFFF0000#);

end Numeric_Display;