with System.Storage_Elements;
package body Gen_Imported_Global with
SPARK_Mode,
Refined_State => (State => V)
is
pragma Warnings (GNATprove, Off, "assuming correct volatile properties");
pragma Warnings (GNATprove, Off, "assuming no concurrent accesses");
V : Integer with
Size => 32,
Volatile,
Async_Writers => True,
Async_Readers => False,
Effective_Reads => False,
Effective_Writes => False,
Address => System.Storage_Elements.To_Address (16#8000_0000#);
pragma Warnings (GNATprove, On, "assuming correct volatile properties");
pragma Warnings (GNATprove, On, "assuming no concurrent accesses");
procedure Set_Global_Twice is
begin
Set_Global;
Set_Global;
end Set_Global_Twice;
procedure Set_Global_Conditionally (X : Boolean) with
Refined_Global => (Output => V),
Refined_Depends => (V => X)
is
begin
if X then
Set_Global;
else
V := 42;
end if;
end Set_Global_Conditionally;
end Gen_Imported_Global;