Aspect programming

[Anh Vo <anhvofrcaus@gmail.com>]

If I understand the ARM 2012 and Ada 2012 Rationale correctly, the
following test code should raise Ada.Assertions.Assertion_Error.
However, Stack_Error is raised instead. I am using GNAT-GPL-2011. Is
it my bug or compiler's bug?


pragma Assertion_Policy (Check);
--  pragma Check_Policy (Postconditions, On);
--  pragma Check_Policy (Preconditions, On);

with Ada.Assertions;
with Ada.Text_Io;
with Ada.Exceptions;
with Stacks;

procedure Aspect_Programming_Test is

   use Ada;
   use Text_Io;

   package Int_Stacks is new Stacks (Integer);
   My_Int_Stack : Int_Stacks.Stack;
   My_Int : Integer := -1;

begin
   Put_Line ("Learning Aspect-Oriented Software Programming");

   for Index in 1 .. 10 loop
      My_Int_Stack.Push (Index);
   end loop;

   Put_Line ("Next Push operation will trigger Stack Full problem /
exception");
   My_Int_Stack.Push (1);

   for Index in 1 .. 10 loop
      My_Int_Stack.Pop (My_Int);
   end loop;

   Put_Line ("Next Pop operation will trigger Stack Empty problem /
exception");
   My_Int_Stack.Pop (My_Int);

exception
   when Ada.Assertions.Assertion_Error =>
      Put_Line ("Pragma Assertion_Policy is in effect");

   when Error : Int_Stacks.Stack_Error =>
      Put_Line ("Pragma Assertion_Policy is ignored");
      Put_Line (Exceptions.Exception_Information (Error));

   when Error : others =>
      Put_Line ("Let's see what is going on => ");
      Put_Line (Exceptions.Exception_Information (Error));

end Aspect_Programming_Test;

generic
   type Item is private;
   Size : Positive := 10;
package Stacks is

   type Stack is tagged private;

   function Is_Empty (S : Stack) return Boolean;

   function Is_Full (S : Stack) return Boolean;

   procedure Push (S : in out Stack;
                   X : in     Item)
      with Pre => not Is_Full (S),
           Post => not Is_Empty (S);

   procedure Pop (S : in out Stack;
                  X :    out Item)
      with Pre => not Is_Empty (S),
           Post => not Is_Full (S);

   Stack_Error: exception;

private

   type Data_Array is array (Natural Range 1 .. Size) of Item;

   type Stack is tagged record
      Data : Data_Array;
      Index : Positive := 1;
   end record;

   function Current_Items (S : Stack) return Natural;

end Stacks;

pragma Assertion_Policy (Check);

package body Stacks is

   protected Mutex is -- Mutex object section starts
      entry Take;
      procedure Release;
   private
      Resource_Available : Boolean := True;
   end Mutex;
   protected body Mutex is
      entry Take when Resource_Available is
      begin
         Resource_Available := False;
      end Take;

      procedure Release is
      begin
         Resource_Available := True;
      end Release;
   end Mutex;  -- Mutex object section ends

   function Is_Empty (S : Stack) return Boolean is
      Condition : Boolean := True;
   begin
      Mutex.Take;
      Condition := S.Index = 1;
      Mutex.Release;
      return Condition;
   end Is_Empty;

   function Is_Full (S : Stack) return Boolean is
      Condition : Boolean := True;
   begin
      Mutex.Take;
      Condition := S.Index = Size + 1;
      Mutex.Release;
      return Condition;
   end Is_Full;

   procedure Push (S : in out Stack;
                   X : in     Item)  is
   begin
      Mutex.Take;
      if S.Index = Size + 1 then
         Mutex.Release;
         raise Stack_Error with "Stack is full!!!";
      end if;
      S.Data(S.Index) := X;
      S.Index := S.Index + 1;
      Mutex.Release;
   end Push;

   procedure Pop (S : in out Stack;
                  X :    out Item)  is
   begin
      Mutex.Take;
      if S.Index = 1 then
         Mutex.Release;
         raise Stack_Error with "Stack is empty!!!";
      end if;
      S.Index := S.Index - 1;
      X := S.Data(S.Index);
      Mutex.Release;
   end Pop;

   function Current_Items (S : Stack) return Natural is
      Items_Count : Natural := 0;
   begin
      Mutex.Take;
      Items_Count := S.Index - 1;
      Mutex.Release;
      return Items_Count;
   end Current_Items;

end Stacks;