blob: c4a38499bc2a9fea996260671b18c50cc161eeca [file] [log] [blame]
-- { 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;