gcc/testsuite/gnat.dg/bip_overlay.adb


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

--  { dg-do compile }

with System;

package body BIP_Overlay
with
   SPARK_Mode
is
   function Init return X
   is
   begin
      return Result : X do
         Result.E := 0;
      end return;
   end Init;

   I : X := Init
   with
      Volatile,
      Async_Readers,
      Address => System'To_Address (16#1234_5678#);

end BIP_Overlay;