The GNAT-defined aspect Predicate has the same semantics as the Ada
aspect Dynamic_Predicate, including direct visibility to the components
of a record type to which the aspect applies.

The following must compile quietly:

   gcc -c integer_stacks.ads

----
pragma SPARK_Mode (On);

with Bounded_Stacks;
package Integer_Stacks is
     new Bounded_Stacks (Element => Integer, Default_Element => 0);
----
generic
   type Element is private;
   Default_Element : Element;
package Bounded_Stacks is

   type Stack (Capacity : Positive) is tagged private
      with Default_Initial_Condition => Empty (Stack);

   function "=" (Left, Right : Stack) return Boolean;

   function Extent (This : Stack) return Natural;

   function Empty (This : Stack) return Boolean;

   function Full (This : Stack) return Boolean;

   procedure Reset (This : out Stack) with
     Post'Class => Empty (This) and
                   not Full (This),
     Global     => null,
     Depends    => (This =>+ null);

   procedure Push (This : in out Stack;  Item : Element) with
     Pre'Class  => not Full (This) and
                   Extent (This) < This.Capacity,
     Post'Class => not Empty (This) and
                   Extent (This) = Extent (This'Old) + 1,
     Global     => null,
     Depends    => (This =>+ Item);

   procedure Pop (This : in out Stack;  Item : out Element) with
     Pre'Class  => not Empty (This),
     Post'Class => not Full (This) and
                   Extent (This) = Extent (This'Old) - 1,
     Global     => null,
     Depends    => (This =>+ null, Item => This);

   function Peek (This : Stack) return Element with
     Pre'Class => not Empty (This),
     Global    => null,
     Depends   => (Peek'Result => This);

private

   type Contents is array (Positive range <>) of Element;

   type Stack (Capacity : Positive) is tagged record
      Values : Contents (1 .. Capacity); -- := (others => Default_Element);
--        Top    : Natural;
      Top    : Natural := 0;
   end record with Predicate => Top <= Capacity,
     Annotate => (GNATprove,
                  Intentional,
                  "type ""Stack"" is not fully initialized",
                  "Because zeroing Top is sufficient");

end Bounded_Stacks;
----
package body Bounded_Stacks is

   ------------
   -- Extent --
   ------------

   function Extent (This : Stack) return Natural is
     (This.Top);

   -----------
   -- Empty --
   -----------

   function Empty (This : Stack) return Boolean is
     (This.Top = 0);

   ----------
   -- Full --
   ----------

   function Full (This : Stack) return Boolean is
     (This.Top = This.Capacity);

   -----------
   -- Reset --
   -----------

   procedure Reset (This : out Stack) is
   begin
      This := (This.Capacity, Top => 0, others => <>);
--        This.Top := 0;
   end Reset;

   ----------
   -- Push --
   ----------

   procedure Push (This : in out Stack;  Item : Element) is
   begin
      This.Top := This.Top + 1;
      This.Values (This.Top) := Item;
   end Push;

   ---------
   -- Pop --
   ---------

   procedure Pop (This : in out Stack;  Item : out Element) is
   begin
      Item := This.Values (This.Top);
      This.Top := This.Top - 1;
   end Pop;

   ----------
   -- Peek --
   ----------

   function Peek (This : Stack) return Element is
     (This.Values (This.Top));

   ---------
   -- "=" --
   ---------

   function "=" (Left, Right : Stack) return Boolean is
   begin
      if Left.Top /= Right.Top then
         return False;
      else
         for K in 1 .. Left.Top loop
            if Left.Values (K) /= Right.Values (K) then
               return False;
            end if;
         end loop;
         return True;
      end if;
   end "=";

end Bounded_Stacks;
----

2018-12-11  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

	* sem_ch13.adb (Check_Aspect_At_End_Of_Declarations,
	Freeze_Entity_Checks): Process aspect Predicate in the same
	fashion as aspect Dynamic_Predicate.

From-SVN: r266985