gnatcheck -P debug.gpr -rules -from=gnatcheck_list.txt

project Debug is
  for Object_Dir use "debug";
  for Main use ("main");
 
  package Builder is
    for Default_Switches ("Ada")
        use ("-g");
    for Executable ("main.adb") use "post_pre_condition";
  end Builder;
 
  package Compiler is
    for Default_Switches ("Ada")
       use ("-fstack-check",
            "-gnata",
            "-gnato",
            "-gnatE");
  end Compiler;
end Debug;
 

with Ada.Text_IO; use Ada.Text_IO;
with Ada.Strings.Fixed;
with Ada.Strings.Unbounded;
with Ada.Characters.Latin_1;
with Stack;
procedure Main is
 
   package String_U renames Ada.Strings.Unbounded;
   package String_F renames Ada.Strings.Fixed;
 
   procedure Print_Element (S : in String_U.Unbounded_String) is
   begin
      Ada.Text_IO.Put (String_U.To_String (S));
   end Print_Element;
 
   package String_Stack is new Stack
     (Size  => 100,
      Elem  => String_U.Unbounded_String,
      Print => Print_Element);
 
   Stack : String_Stack.Stack;
 
begin
 
   Ada.Text_IO.Put_Line ("Fill Stack");
   Stack.Push (String_U.To_Unbounded_String ("string 1"));
   Stack.Push (String_U.To_Unbounded_String ("string 2"));
 
   Ada.Text_IO.Put_Line ("Print_All");
   Stack.Print_All;
 
   Ada.Text_IO.Put_Line ("Pop First");
   Ada.Text_IO.Put_Line (String_U.To_String (Stack.Pop));
   Ada.Text_IO.Put_Line ("Pop Second");
   Ada.Text_IO.Put_Line (String_U.To_String (Stack.Pop));
   Ada.Text_IO.Put_Line ("Pop Third that will generate ASSERT_FAILURE");
   Ada.Text_IO.Put_Line (String_U.To_String (Stack.Pop));
 
end Main;
 

with Ada.Containers.Vectors;
generic
   Size : Integer;
   type Elem is private;
 
   with procedure Print (E : in Elem);
 
package Stack is
   type Stack is tagged limited private;
 
   subtype Count_Type is Integer range 0 .. Size;
   subtype Index_Type is Count_Type range 1 .. Size;
   package Stack_Vectors is new Ada.Containers.Vectors
     (Index_Type   => Index_Type,
      Element_Type => Elem);
 
   -- Use of precondition ( only available in ada 2012 )
   -- Add an element in the stack
   procedure Push (This : in out Stack; E : in Elem) with
      Pre => not This.Is_Full;
 
   -- Use of precondition ( only available in ada 2012 )
   -- Retrieve an element in the stack
   function Pop (This : in out Stack) return Elem with
      Pre => not This.Is_Empty;
 
   -- Use of precondition ( only available in ada 2012 )
   -- Retrieve an element in the stack
   procedure Pop (This : in out Stack; E : out Elem) with
      Pre => not This.Is_Empty;
 
   -- Use of precondition ( only available in ada 2012 )
   -- Retrieve an element in the stack
   procedure Pop (This : in out Stack) with
      Pre => not This.Is_Empty;
 
   -- Use of precondition ( only available in ada 2012 )
   -- Retrieve one or more element in the stack until E is Found
   procedure Pop_Until (This : in out Stack; E : in Elem) with
      Pre => not This.Is_Empty;
   procedure Print_All (This : in Stack);
   function Length (This : in Stack) return Count_Type;
   function Is_Full (This : in out Stack) return Boolean;
   function Is_Empty (This : in out Stack) return Boolean;
 
private
   type Stack is tagged limited record
      Len : Count_Type := 0;
      V   : Stack_Vectors.Vector;
   end record;
end Stack;
 

with Ada.Text_IO; use Ada.Text_IO;
 
package body Stack is
   procedure Push (This : in out Stack; E : in Elem) is
   begin
      This.Len := This.Len + 1;
      Stack_Vectors.Append (This.V, E);
   end Push;
 
   procedure Pop (This : in out Stack; E : out Elem) is
   begin
      E := Stack_Vectors.Last_Element (This.V);
      Stack_Vectors.Delete_Last (This.V);
      This.Len := This.Len - 1;
   end Pop;
 
   function Pop (This : in out Stack) return Elem is
      Element : Elem;
   begin
      This.Pop (Element);
      return Element;
   end Pop;
 
   -- pop until E is found
   procedure Pop_Until (This : in out Stack; E : in Elem) is
      Element : Elem;
 
      Nb_Deleted_Item : Ada.Containers.Count_Type := 0;
      Length          : Count_Type                := This.Len;
      Found           : Boolean                   := False;
      End_Of_Stack    : Boolean                   := False;
      Pop_Cursor      : Stack_Vectors.Cursor      := Stack_Vectors.Last (This.V);
      use Ada.Containers;
 
   begin
 
      while not Found and not End_Of_Stack loop
 
         if Length = 0 then
            End_Of_Stack := True;
         else
            Nb_Deleted_Item := Nb_Deleted_Item + 1;
            Length          := Length - 1;
            Element         := Stack_Vectors.Element (Pop_Cursor);
            if (E = Element) then
               Found := True;
            end if;
            Pop_Cursor := Stack_Vectors.Previous (Pop_Cursor);
         end if;
      end loop;
 
      if (Found) then
 
         Stack_Vectors.Delete_Last (This.V, Nb_Deleted_Item);
         This.Len := This.Len - Count_Type (Nb_Deleted_Item);
      else
         Put ("Pop_Until Error:");
         Print (E);
         Put ("  Stack :");
         Print_All (This => This);
         Put_Line ("");
      end if;
   end Pop_Until;
 
   procedure Pop (This : in out Stack) is
   begin
      Stack_Vectors.Delete_Last (This.V);
      This.Len := This.Len - 1;
   end Pop;
 
   procedure Print_All (This : in Stack) is
   begin
      if (This.Len > 0) then
         for I in 1 .. This.Len - 1 loop
            Print (Stack_Vectors.Element (This.V, I));
            Put (":");
         end loop;
         Print (Stack_Vectors.Element (This.V, This.Len));
         Put_Line ("");
      else
         Put_Line ("Empty Stack");
      end if;
   end Print_All;
 
   function Length (This : in Stack) return Count_Type is
   begin
      return This.Len;
   end Length;
 
   function Is_Full (This : in out Stack) return Boolean is
   begin
      return This.Len = Size;
   end Is_Full;
 
   function Is_Empty (This : in out Stack) return Boolean is
   begin
      return This.Len = 0;
   end Is_Empty;
 
end Stack;