--
-- Copyright (C) 2015-2016 secunet Security Networks AG
--
-- This program is free software; you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation; either version 2 of the License, or
-- (at your option) any later version.
--
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.
--

package HW.Time
   with Abstract_State => (State with External => Async_Writers)
is

   type T is private;

   function Now return T
   with
      Volatile_Function,
      Global => (Input => State);

   function US_From_Now (US : Natural) return T
   with
      Volatile_Function,
      Global => (Input => State);

   function MS_From_Now (MS : Natural) return T
   with
      Volatile_Function,
      Global => (Input => State);

   function Now_US return Int64
   with
      Volatile_Function,
      Global => (Input => State);

   ----------------------------------------------------------------------------

   pragma Warnings
     (GNATprove, Off, "subprogram ""*Delay*"" has no effect",
      Reason => "No effect on dataflow but time always passes.");

   -- Delay execution until Deadline has been reached.
   procedure Delay_Until (Deadline : T)
   with
      Global => (Input => State);

   procedure U_Delay (US : Natural)
   with
      Global => (Input => State);

   procedure M_Delay (MS : Natural)
   with
      Global => (Input => State);

   pragma Warnings
     (GNATprove, On, "subprogram ""*Delay*"" has no effect");

   ----------------------------------------------------------------------------

   function Timed_Out (Deadline : T) return Boolean
   with
      Volatile_Function,
      Global => (Input => State);

private

   type T is new Word64;

end HW.Time;

--  vim: set ts=8 sts=3 sw=3 et: