From f5d4b6ab396f6d92ead4a356fe0b4dfdd15c332e Mon Sep 17 00:00:00 2001
From: Ed Schonberg <schonberg@adacore.com>
Date: Tue, 11 Dec 2018 11:09:46 +0000
Subject: [PATCH] [Ada] Spurious visibility error on aspect Predicate

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
---
 gcc/ada/ChangeLog    | 6 ++++++
 gcc/ada/sem_ch13.adb | 2 ++
 2 files changed, 8 insertions(+)

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5169d0a..50f53b8 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2018-12-11  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb (Check_Aspect_At_End_Of_Declarations,
+	Freeze_Entity_Checks): Process aspect Predicate in the same
+	fashion as aspect Dynamic_Predicate.
+
 2018-12-11  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* gcc-interface/trans.c (elaborate_all_entities_for_package):
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index e1bc6bc..fb8dff0 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -9364,6 +9364,7 @@ package body Sem_Ch13 is
          --  components and discriminants of the type.
 
          elsif A_Id  = Aspect_Dynamic_Predicate
+           or else A_Id = Aspect_Predicate
            or else A_Id = Aspect_Priority
          then
             Push_Type (Ent);
@@ -11252,6 +11253,7 @@ package body Sem_Ch13 is
                then
                   A_Id := Get_Aspect_Id (Ritem);
                   if A_Id = Aspect_Dynamic_Predicate
+                    or else A_Id = Aspect_Predicate
                     or else A_Id = Aspect_Priority
                   then
                     --  Retrieve the visibility to components and discriminants
-- 
2.7.4