gcc/testsuite/gnat.dg/predicate8_pkg.adb

   1 pragma Spark_Mode (On);
   2
   3 package body Predicate8_Pkg is
   4    function Empty
   5      (Buffer : in Ring_Buffer_Type) return Boolean
   6    is (Size (Buffer) = 0);
   7
   8    function Full
   9      (Buffer : in Ring_Buffer_Type) return Boolean
  10    is (Size (Buffer) = Buffer.Max_Size);
  11
  12    function Size
  13      (Buffer : in Ring_Buffer_Type) return Natural
  14    is (Buffer.Count);
  15
  16    function Free
  17      (Buffer : in Ring_Buffer_Type) return Natural
  18    is (Buffer.Max_Size - Size (Buffer));
  19
  20    function First
  21      (Buffer : in Ring_Buffer_Type) return Element_Type
  22    is (Buffer.Items (Buffer.Head));
  23
  24    function Last
  25      (Buffer : in Ring_Buffer_Type) return Element_Type
  26    is (Buffer.Items (Buffer.Tail));
  27
  28    procedure Get
  29      (Buffer   : in out Ring_Buffer_Type;
  30       Element  :    out Element_Type)
  31    is
  32    begin
  33       Element := Buffer.Items (Buffer.Head);
  34       Buffer  :=
  35         Buffer'Update
  36           (Head  =>
  37             (if Buffer.Head = Buffer.Max_Size then 1 else Buffer.Head + 1),
  38            Count => Buffer.Count - 1);
  39    end Get;
  40
  41    procedure Put
  42      (Buffer   : in out Ring_Buffer_Type;
  43       Element  : in     Element_Type)
  44    is
  45     begin
  46       if Buffer.Tail = Buffer.Max_Size then
  47          Buffer.Tail := 1;
  48       else
  49          Buffer.Tail := Buffer.Tail + 1;
  50       end if;
  51
  52       Buffer.Items (Buffer.Tail) := Element;
  53       Buffer.Count := Buffer.Count + 1;
  54    end Put;
  55
  56    procedure Clear
  57      (Buffer : in out Ring_Buffer_Type)
  58    is
  59    begin
  60       Buffer.Head  := 1;
  61       Buffer.Tail  := Buffer.Max_Size;
  62       Buffer.Count := 0;
  63    end Clear;
  64 end Predicate8_Pkg;