gcc/testsuite/gnat.dg/bip_overlay.ads

   1 package BIP_Overlay
   2  with SPARK_Mode
   3 is
   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
  13 private
  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;
  22 end BIP_Overlay;