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