1pragma Restrictions (No_Exception_Propagation);
2
3package Ghost7 is
4   type Word64 is mod 2**64;
5   type My_Array_Type is array (Word64) of Boolean;
6   My_Array : My_Array_Type with Ghost;
7   procedure Dummy;
8end Ghost7;