initialize stack with default null element

ref #18

Author: jklmnn

src/basalt-stack.adb

@@ -34,8 +34,8 @@ is
    procedure Push (S : in out Context;
                    E :        Element_Type) is
    begin
-      S.Index := S.Index + 1;
-      S.List (S.Index) := E;
+      S.Index                := S.Index + 1;
+      S.List (S.Index).Value := E;
    end Push;
 
    ------------------
@@ -46,7 +46,7 @@ is
    is
    begin
       S.Index := S.Index + 1;
-      Push (S.List (S.Index));
+      Push (S.List (S.Index).Value);
    end Generic_Push;
 
    ---------
@@ -56,7 +56,7 @@ is
    procedure Pop (S : in out Context;
                   E :    out Element_Type) is
    begin
-      E := S.List (S.Index);
+      E := S.List (S.Index).Value;
       Drop (S);
    end Pop;
 
@@ -67,7 +67,7 @@ is
    procedure Generic_Pop (S : in out Context)
    is
    begin
-      Pop (S.List (S.Index));
+      Pop (S.List (S.Index).Value);
       Drop (S);
    end Generic_Pop;
 
@@ -93,19 +93,10 @@ is
    -- Initialize --
    ----------------
 
-   procedure Initialize (S            : out Context;
-                         Null_Element :     Element_Type)
+   procedure Initialize (S : in out Context)
    is
    begin
       S.Index := 0;
-      --  This would be the correct way to initialize S.List:
-      --     S.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 S.List loop
-         pragma Loop_Invariant (S.Index = 0);
-         E := Null_Element;
-      end loop;
    end Initialize;
 
 end Basalt.Stack;

src/basalt-stack.ads

@@ -11,6 +11,7 @@
 
 generic
    type Element_Type is private;
+   Null_Element : Element_Type;
 package Basalt.Stack with
    SPARK_Mode,
    Pure,
@@ -106,21 +107,20 @@ is
    --  Initialize stack and clear stack buffer
    --
    --  @param S  Stack
-   procedure Initialize (S            : out Context;
-                         Null_Element :     Element_Type) with
+   procedure Initialize (S : in out Context) with
      Post => Is_Empty (S)
              and then not Is_Full (S);
 
-   pragma Annotate (GNATprove, False_Positive,
-                    """S.List"" might not be initialized*",
-                    "Initialized in complete loop");
-
 private
 
-   type Simple_List is array (Positive range <>) of Element_Type;
+   type List_Element is record
+      Value : Element_Type := Null_Element;
+   end record;
+
+   type Simple_List is array (Positive range <>) of List_Element;
 
    type Context (Size : Positive) is record
-      Index : Natural;
+      Index : Natural := 0;
       List  : Simple_List (1 .. Size);
    end record with
      Predicate => Index <= List'Last;

test/aunit/stack_tests.adb

@@ -3,15 +3,15 @@ with Basalt.Stack;
 
 package body Stack_Tests
 is
-   package F is new Basalt.Stack (Integer);
+   package F is new Basalt.Stack (Integer, 0);
 
    procedure Test_Stack (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.Push (Q, I);
       end loop;
@@ -26,7 +26,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.Push (Q, 1);
       Aunit.Assertions.Assert (F.Count (Q) = 1, "Count not 1 after Push");
@@ -43,7 +43,7 @@ is
       pragma Unreferenced (T);
       Q : F.Context (1);
    begin
-      F.Initialize (Q, 0);
+      F.Initialize (Q);
       Aunit.Assertions.Assert (F.Is_Empty (Q), "Stack not empty");
       Aunit.Assertions.Assert (F.Count (Q) = 0, "Stack not empty");
       F.Push (Q, 1);
@@ -59,7 +59,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.Push (Q, I);
@@ -91,10 +91,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");
@@ -120,7 +120,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");
       Push (Q);
       Aunit.Assertions.Assert (F.Count (Q) = 1, "Count should be 1");

test/proof/proof_stack.adb

@@ -5,7 +5,7 @@ package body Proof_Stack with
    SPARK_Mode
 is
 
-   package Stack is new Basalt.Stack (Integer);
+   package Stack is new Basalt.Stack (Integer, 0);
    S : Stack.Context (10);
 
    procedure Prove
@@ -26,7 +26,7 @@ is
          J_Ignore := I;
       end Pop;
    begin
-      Stack.Initialize (S, 0);
+      Stack.Initialize (S);
       for I in Integer range 7 .. 13 loop
          Stack.Push (S, I);
          exit when Stack.Count (S) >= Stack.Size (S);