gnatprove_13.2.1_28fc3583/share/examples/spark/gnatprove_by_example/ug__volatile_example_a/volatile_example_a.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
25
26
27
28
29
30
31
32
33
with System.Storage_Elements;
package body Volatile_Example_A
  with SPARK_Mode
is
   type Pair is record
      X, Y : Integer;
   end record;

   V : Integer
     with Volatile,
          Address  => System.Storage_Elements.To_Address (16#DEAD_BEEF#),
          Warnings => Off;

   W : Pair
     with Volatile,
          Address  => System.Storage_Elements.To_Address (16#00C0_FFEE#),
          Warnings => Off;

   procedure Do_Stuff
     with Global => (In_Out => (V, W));

   procedure Do_Stuff is
      Tmp : Pair;
   begin
      Tmp := W;  --  composite volatiles must be read and assigned whole
      if (Tmp.X > 0) then
         Tmp.X := V;
         Tmp.Y := V;
         pragma Assert (Tmp.X = Tmp.Y); -- not provable
      end if;
      W := Tmp;
   end Do_Stuff;
end Volatile_Example_A;