1package BIP_Overlay
2 with SPARK_Mode
3is
4   type X (<>) is limited private;
5
6   pragma Warnings (gnatprove, Off,
7     "volatile function ""Init"" has no volatile effects",
8      reason => "Init is a pure function but returns a volatile type.");
9   function Init return X
10   with
11      Volatile_Function;
12
13private
14   type A is limited record
15      E : Integer;
16   end record
17      with
18      Volatile;
19      -- and Async_Readers when implemented;
20
21   type X is limited new A;
22end BIP_Overlay;
23