bbqueue_0.3.2_5e5007cf/tests/src/main_framed.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
with Ada.Text_IO; use Ada.Text_IO;

with System.Storage_Elements; use System.Storage_Elements;
with BBqueue;
with BBqueue.Buffers.framed;
with System; use System;

procedure Main_Framed
with SPARK_Mode
is
   use type BBqueue.Result_Kind;

   Q : aliased BBqueue.Buffers.framed.Framed_Buffer (60);

   procedure Fill_With_CB (Request, Actual : BBqueue.Count;
                           Val : Storage_Element);
   procedure Print_Content_With_CB;

   ------------------
   -- Fill_With_CB --
   ------------------

   procedure Fill_With_CB (Request, Actual : BBqueue.Count;
                           Val             : Storage_Element)
   is
      pragma SPARK_Mode (Off);

      procedure Process_Write (Data      : out Storage_Array;
                               To_Commit : out BBqueue.Count);

      procedure Process_Write (Data      : out Storage_Array;
                               To_Commit : out BBqueue.Count)
      is
      begin
         Put_Line ("Fill" & Actual'Img & " bytes.");
         Data (Data'First .. Data'First + Actual - 1) := (others => Val);
         To_Commit := Actual;
      end Process_Write;

      procedure Write is new BBqueue.Buffers.framed.Write_CB (Process_Write);
      Result : BBqueue.Result_Kind;
   begin
      Write (Q, Request, Result);
      if Result /= BBqueue.Valid then
         Put_Line ("Write failed: " & Result'Img);
      end if;
   end Fill_With_CB;

   ---------------------------
   -- Print_Content_With_CB --
   ---------------------------

   procedure Print_Content_With_CB is
      procedure Process_Read (Data : Storage_Array);

      procedure Process_Read (Data : Storage_Array) is
      begin
         Put ("Print" & Data'Length'Img & " bytes -> ");
         for Elt of Data loop
            Put (Elt'Img);
         end loop;
         New_Line;
      end Process_Read;

      procedure Read is new BBqueue.Buffers.framed.Read_CB (Process_Read);
      Result : BBqueue.Result_Kind;
   begin
      Read (Q, Result);
      if Result /= BBqueue.Valid then
         Put_Line ("Read failed: " & Result'Img);
      end if;
   end Print_Content_With_CB;

   V : Storage_Element := 1;
begin

   Put_Line ("Count'Object_Size:" & BBqueue.Count'Object_Size'Img);

   for X in BBqueue.Count range 1 .. 4 loop
      Put_Line ("-- Loop" & X'Img & " --");
      Fill_With_CB (10, X, V);
      Fill_With_CB (20, X * 2, V * 2);
      V := V + 1;
      Print_Content_With_CB;
      Print_Content_With_CB;
   end loop;
end Main_Framed;