File : a-exetim-bb.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                   A D A . E X E C U T I O N _ T I M E                    --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 -- This specification is derived from the Ada Reference Manual for use with --
  10 -- GNAT.  In accordance with the copyright of that document, you can freely --
  11 -- copy and modify this specification,  provided that if you redistribute a --
  12 -- modified version,  any changes that you have made are clearly indicated. --
  13 --                                                                          --
  14 ------------------------------------------------------------------------------
  15 
  16 with Ada.Task_Identification;
  17 with Ada.Real_Time;
  18 
  19 package Ada.Execution_Time with
  20   SPARK_Mode
  21 is
  22 
  23    type CPU_Time is private;
  24 
  25    CPU_Time_First : constant CPU_Time;
  26    CPU_Time_Last  : constant CPU_Time;
  27    CPU_Time_Unit  : constant := Ada.Real_Time.Time_Unit;
  28    CPU_Tick       : constant Ada.Real_Time.Time_Span;
  29 
  30    use type Ada.Task_Identification.Task_Id;
  31 
  32    function Clock
  33      (T : Ada.Task_Identification.Task_Id :=
  34         Ada.Task_Identification.Current_Task)
  35       return CPU_Time
  36    with
  37      Volatile_Function,
  38      Global => Ada.Real_Time.Clock_Time,
  39      Pre    => T /= Ada.Task_Identification.Null_Task_Id;
  40 
  41    function "+"
  42      (Left  : CPU_Time;
  43       Right : Ada.Real_Time.Time_Span) return CPU_Time
  44    with
  45      Global => null;
  46 
  47    function "+"
  48      (Left  : Ada.Real_Time.Time_Span;
  49       Right : CPU_Time) return CPU_Time
  50    with
  51      Global => null;
  52 
  53    function "-"
  54      (Left  : CPU_Time;
  55       Right : Ada.Real_Time.Time_Span) return CPU_Time
  56    with
  57      Global => null;
  58 
  59    function "-"
  60      (Left  : CPU_Time;
  61       Right : CPU_Time) return Ada.Real_Time.Time_Span;
  62 
  63    function "<"  (Left, Right : CPU_Time) return Boolean with
  64      Global => null;
  65    function "<=" (Left, Right : CPU_Time) return Boolean with
  66      Global => null;
  67    function ">"  (Left, Right : CPU_Time) return Boolean with
  68      Global => null;
  69    function ">=" (Left, Right : CPU_Time) return Boolean with
  70      Global => null;
  71 
  72    procedure Split
  73      (T  : CPU_Time;
  74       SC : out Ada.Real_Time.Seconds_Count;
  75       TS : out Ada.Real_Time.Time_Span)
  76    with
  77      Global => null;
  78 
  79    function Time_Of
  80      (SC : Ada.Real_Time.Seconds_Count;
  81       TS : Ada.Real_Time.Time_Span := Ada.Real_Time.Time_Span_Zero)
  82       return CPU_Time
  83    with
  84      Global => null;
  85 
  86    Interrupt_Clocks_Supported          : constant Boolean := True;
  87    Separate_Interrupt_Clocks_Supported : constant Boolean := True;
  88 
  89    function Clock_For_Interrupts return CPU_Time with
  90      Volatile_Function,
  91      Global => Ada.Real_Time.Clock_Time,
  92      Pre    => Interrupt_Clocks_Supported;
  93 
  94 private
  95    pragma SPARK_Mode (Off);
  96 
  97    type CPU_Time is new Ada.Real_Time.Time;
  98 
  99    CPU_Time_First : constant CPU_Time  := CPU_Time (Ada.Real_Time.Time_First);
 100    CPU_Time_Last  : constant CPU_Time  := CPU_Time (Ada.Real_Time.Time_Last);
 101 
 102    CPU_Tick : constant Ada.Real_Time.Time_Span := Ada.Real_Time.Tick;
 103 
 104    pragma Import (Intrinsic, "<");
 105    pragma Import (Intrinsic, "<=");
 106    pragma Import (Intrinsic, ">");
 107    pragma Import (Intrinsic, ">=");
 108 
 109 end Ada.Execution_Time;