gcc/testsuite/gnat.dg/bip_overlay.adb

   1 --  { dg-do compile }
   2
   3 with System;
   4
   5 package body BIP_Overlay
   6 with
   7    SPARK_Mode
   8 is
   9    function Init return X
  10    is
  11    begin
  12       return Result : X do
  13          Result.E := 0;
  14       end return;
  15    end Init;
  16
  17    I : X := Init
  18    with
  19       Volatile,
  20       Async_Readers,
  21       Address => System'To_Address (16#1234_5678#);
  22
  23 end BIP_Overlay;