initialize queue with default null element

Author: jklmnn

src/basalt-queue.adb

@@ -20,17 +20,9 @@ is
    function Put_Index (C : Context) return Positive is
       (Positive ((C.Index + C.Length - 1) mod C.List'Length + Long_Positive (C.List'First)));
 
-   procedure Initialize (C            : out Context;
-                         Null_Element :     T)
+   procedure Initialize (C : in out Context)
    is
    begin
-      --  This would be the correct way to initialize S.List:
-      --     C.List  := (others => Null_Element);
-      --  As this creates a (potentially large) object on the stack, we initialize in a loop. The resulting flow
-      --  error is justified in the spec.
-      for E of C.List loop
-         E := Null_Element;
-      end loop;
       C.Length := Long_Natural'First;
       C.Index  := Long_Natural'First;
    end Initialize;
@@ -39,28 +31,28 @@ is
                   Element :        T)
    is
    begin
-      C.Length       := C.Length + 1;
-      C.List (Put_Index (C)) := Element;
+      C.Length                     := C.Length + 1;
+      C.List (Put_Index (C)).Value := Element;
    end Put;
 
    procedure Generic_Put (C : in out Context)
    is
    begin
-      C.Length       := C.Length + 1;
-      Put (C.List (Put_Index (C)));
+      C.Length := C.Length + 1;
+      Put (C.List (Put_Index (C)).Value);
    end Generic_Put;
 
    procedure Peek (C       :     Context;
                    Element : out T)
    is
    begin
-      Element := C.List (Positive (C.Index + Long_Positive (C.List'First)));
+      Element := C.List (Positive (C.Index + Long_Positive (C.List'First))).Value;
    end Peek;
 
    procedure Generic_Peek (C : Context)
    is
    begin
-      Peek (C.List (Positive (C.Index + Long_Positive (C.List'First))));
+      Peek (C.List (Positive (C.Index + Long_Positive (C.List'First))).Value);
    end Generic_Peek;
 
    procedure Drop (C : in out Context)

src/basalt-queue.ads

@@ -14,6 +14,7 @@
 
 generic
    type T is private;
+   Null_Element : T;
 package Basalt.Queue with
    SPARK_Mode,
    Pure,
@@ -41,20 +42,11 @@ is
    --  @return   Number of elements currently in the queue
    function Count (C : Context) return Natural;
 
-   --  Initializes the queue with a default element value
+   --  Initializes the queue
    --
-   --  This procedure is only needed to proof the data flow. It is
-   --  the only way to assign a Queue object. The object will automatically
-   --  be initialized with the given element. The initialized queue will be empty.
-   --
-   --  @param C             Queue context
-   --  @param Null_Element  Default element to initialize the queue with
-   procedure Initialize (C            : out Context;
-                         Null_Element :     T) with
+   --  @param C  Queue context
+   procedure Initialize (C : in out Context) with
       Post => Count (C) = 0;
-   pragma Annotate (GNATprove, False_Positive,
-                    """C.List"" might not be initialized*",
-                    "Initialized in complete loop");
 
    --  Puts an element in the queue.
    --
@@ -115,7 +107,11 @@ is
 
 private
 
-   type Simple_List is array (Natural range <>) of T;
+   type List_Element is record
+      Value : T := Null_Element;
+   end record;
+
+   type Simple_List is array (Natural range <>) of List_Element;
    subtype Long_Natural is Long_Integer range 0 .. Long_Integer'Last;
    subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last;
 

test/aunit/queue_tests.adb

@@ -4,15 +4,15 @@ with Basalt.Queue;
 
 package body Queue_Tests
 is
-   package F is new Basalt.Queue (Integer);
+   package F is new Basalt.Queue (Integer, 0);
 
    procedure Test_Fifo (T : in out Aunit.Test_Cases.Test_Case'Class)
    is
       pragma Unreferenced (T);
       Q : F.Context (100);
       J : Integer;
    begin
-      F.Initialize (Q, 0);
+      F.Initialize (Q);
       for I in 70 .. 120 loop
          F.Put (Q, I);
       end loop;
@@ -27,7 +27,7 @@ is
       pragma Unreferenced (T);
       Q : F.Context (2);
    begin
-      F.Initialize (Q, 0);
+      F.Initialize (Q);
       Aunit.Assertions.Assert (F.Count (Q) = 0, "Count not 0");
       F.Put (Q, 1);
       Aunit.Assertions.Assert (F.Count (Q) = 1, "Count not 1 after Put");
@@ -45,7 +45,7 @@ is
       Q : F.Context (1);
       J : Integer;
    begin
-      F.Initialize (Q, 0);
+      F.Initialize (Q);
       Aunit.Assertions.Assert (F.Count (Q) = 0, "Queue not empty");
       F.Put (Q, 1);
       Aunit.Assertions.Assert (F.Count (Q) = 1, "Queue not full");
@@ -60,7 +60,7 @@ is
       pragma Unreferenced (T);
       Q : F.Context (100);
    begin
-      F.Initialize (Q, 0);
+      F.Initialize (Q);
       Aunit.Assertions.Assert (F.Count (Q) = 0, "Count should be 0");
       for I in Integer range 1 .. 20 loop
          F.Put (Q, I);
@@ -90,7 +90,7 @@ is
       Q      : F.Context (1);
       Unused : Integer;
    begin
-      F.Initialize (Q, 0);
+      F.Initialize (Q);
       Aunit.Assertions.Assert (F.Count (Q) = 0, "Count should be 0");
       F.Put (Q, 1);
       Aunit.Assertions.Assert (F.Count (Q) = 1, "Count should be 1");
@@ -118,7 +118,7 @@ is
          Aunit.Assertions.Assert (I = 42, "I should be 42");
       end Peek;
    begin
-      F.Initialize (Q, 0);
+      F.Initialize (Q);
       Aunit.Assertions.Assert (F.Count (Q) = 0, "Count should be 0");
       Put (Q);
       Aunit.Assertions.Assert (F.Count (Q) = 1, "Count should be 1");
@@ -136,10 +136,10 @@ is
       Q3 : F.Context (200);
       Q4 : F.Context (13000);
    begin
-      F.Initialize (Q1, 0);
-      F.Initialize (Q2, 0);
-      F.Initialize (Q3, 0);
-      F.Initialize (Q4, 0);
+      F.Initialize (Q1);
+      F.Initialize (Q2);
+      F.Initialize (Q3);
+      F.Initialize (Q4);
       Aunit.Assertions.Assert (F.Size (Q1) = 1, "Size of Q1 should be 1");
       Aunit.Assertions.Assert (F.Size (Q2) = 50, "Size of Q2 should be 50");
       Aunit.Assertions.Assert (F.Size (Q3) = 200, "Size of Q3 should be 200");
@@ -152,7 +152,7 @@ is
       Q : F.Context (10);
       J : Integer;
    begin
-      F.Initialize (Q, 0);
+      F.Initialize (Q);
       for I in Integer range 1 .. 7 loop
          F.Put (Q, I);
       end loop;

test/proof/proof_queue.adb

@@ -5,7 +5,7 @@ package body Proof_Queue with
    SPARK_Mode
 is
 
-   package Fifo is new Basalt.Queue (Integer);
+   package Fifo is new Basalt.Queue (Integer, 0);
    Queue : Fifo.Context (10);
 
    procedure Prove
@@ -27,7 +27,7 @@ is
          J_Ignore := I;
       end Peek;
    begin
-      Fifo.Initialize (Queue, 0);
+      Fifo.Initialize (Queue);
       for I in Integer range 7 .. 13 loop
          Fifo.Put (Queue, I);
          exit when Fifo.Count (Queue) >= Fifo.Size (Queue);