[Ada] Spurious visibility error on dynamic_predicate aspect in generic

This patch fixes a spurious error when verifying that the visibility of
the expression of an aspect has not changed between the freeze point of
the entity to which it applies, and the end of the enclosing declarative
part. If the entity is a composite type its components must be made
directly visible for the analysis of the expression. In a generic
context this must be done explicitly at the end of the declarative part.

2019-07-08  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

	* sem_ch13.adb (Check_Aspect_At_End_Of_Declarations): For an
	unanalized aspect in a generic context that has not been
	analyzed yet, if the aspect applies to a type, place the type on
	the scope stack to make its components visible, before checking
	conformance with the version of the expression analyzed at the
	freeze point.

gcc/testsuite/

	* gnat.dg/predicate8.adb, gnat.dg/predicate8_pkg.adb,
	gnat.dg/predicate8_pkg.ads: New testcase.

From-SVN: r273197

gcc/ada/ChangeLog

+2019-07-08  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb (Check_Aspect_At_End_Of_Declarations): For an
+	unanalized aspect in a generic context that has not been
+	analyzed yet, if the aspect applies to a type, place the type on
+	the scope stack to make its components visible, before checking
+	conformance with the version of the expression analyzed at the
+	freeze point.
+
 2019-07-05  Justin Squirek  <squirek@adacore.com>
 
 	* checks.adb (Apply_Accessibility_Check): Add logic to fetch the

gcc/ada/sem_ch13.adb

@@ -3491,7 +3491,9 @@ package body Sem_Ch13 is
 
                   --  Build the precondition/postcondition pragma
 
-                  --  Add note about why we do NOT need Copy_Tree here???
+                  --  We use Relocate_Node here rather than New_Copy_Tree
+                  --  because subsequent visibility analysis of the aspect
+                  --  depends on this sharing. This should be cleaned up???
 
                   Make_Aitem_Pragma
                     (Pragma_Argument_Associations => New_List (
@@ -9358,10 +9360,20 @@ package body Sem_Ch13 is
 
       else
          --  In a generic context freeze nodes are not always generated, so
-         --  analyze the expression now.
+         --  analyze the expression now. If the aspect is for a type, this
+         --  makes its potential components accessible.
 
          if not Analyzed (Freeze_Expr) and then Inside_A_Generic then
-            Preanalyze (Freeze_Expr);
+            if A_Id = Aspect_Dynamic_Predicate
+              or else A_Id = Aspect_Predicate
+              or else A_Id = Aspect_Priority
+            then
+               Push_Type (Ent);
+               Preanalyze (Freeze_Expr);
+               Pop_Type (Ent);
+            else
+               Preanalyze (Freeze_Expr);
+            end if;
          end if;
 
          --  Indicate that the expression comes from an aspect specification,

gcc/testsuite/ChangeLog

+2019-07-08  Ed Schonberg  <schonberg@adacore.com>
+
+	* gnat.dg/predicate8.adb, gnat.dg/predicate8_pkg.adb,
+	gnat.dg/predicate8_pkg.ads: New testcase.
+
 2019-07-08  Richard Biener  <rguenther@suse.de>
 
 	PR tree-optimization/83518

gcc/testsuite/gnat.dg/predicate8.adb

+--  { dg-do compile }
+
+pragma Spark_Mode (On);
+
+with Predicate8_Pkg;
+
+procedure Predicate8 is
+   package Ring_Buffer is new Predicate8_Pkg (Element_Type => Integer);
+   use Ring_Buffer;
+
+   X : Ring_Buffer_Type (4);
+
+begin
+   Put (X, 1);
+end Predicate8;

gcc/testsuite/gnat.dg/predicate8_pkg.adb

+pragma Spark_Mode (On);
+
+package body Predicate8_Pkg is
+   function Empty
+     (Buffer : in Ring_Buffer_Type) return Boolean
+   is (Size (Buffer) = 0);
+
+   function Full
+     (Buffer : in Ring_Buffer_Type) return Boolean
+   is (Size (Buffer) = Buffer.Max_Size);
+
+   function Size
+     (Buffer : in Ring_Buffer_Type) return Natural
+   is (Buffer.Count);
+
+   function Free
+     (Buffer : in Ring_Buffer_Type) return Natural
+   is (Buffer.Max_Size - Size (Buffer));
+
+   function First
+     (Buffer : in Ring_Buffer_Type) return Element_Type
+   is (Buffer.Items (Buffer.Head));
+
+   function Last
+     (Buffer : in Ring_Buffer_Type) return Element_Type
+   is (Buffer.Items (Buffer.Tail));
+
+   procedure Get
+     (Buffer   : in out Ring_Buffer_Type;
+      Element  :    out Element_Type)
+   is
+   begin
+      Element := Buffer.Items (Buffer.Head);
+      Buffer  :=
+        Buffer'Update
+          (Head  =>
+            (if Buffer.Head = Buffer.Max_Size then 1 else Buffer.Head + 1),
+           Count => Buffer.Count - 1);
+   end Get;
+
+   procedure Put
+     (Buffer   : in out Ring_Buffer_Type;
+      Element  : in     Element_Type)
+   is
+    begin
+      if Buffer.Tail = Buffer.Max_Size then
+         Buffer.Tail := 1;
+      else
+         Buffer.Tail := Buffer.Tail + 1;
+      end if;
+
+      Buffer.Items (Buffer.Tail) := Element;
+      Buffer.Count := Buffer.Count + 1;
+   end Put;
+
+   procedure Clear
+     (Buffer : in out Ring_Buffer_Type)
+   is
+   begin
+      Buffer.Head  := 1;
+      Buffer.Tail  := Buffer.Max_Size;
+      Buffer.Count := 0;
+   end Clear;
+end Predicate8_Pkg;

gcc/testsuite/gnat.dg/predicate8_pkg.ads

+pragma Spark_Mode (On);
+
+generic
+  type Element_Type is private;
+
+package Predicate8_Pkg is
+   pragma Annotate (GNATprove, Terminating, Predicate8_Pkg);
+
+   subtype Small_Natural  is Natural range 0 .. Natural'Last / 2;
+   subtype Small_Positive is Natural range 1 .. Natural'Last / 2;
+
+   type Element_Array_Type is array (Small_Positive range <>) of Element_Type;
+
+   type Ring_Buffer_Type (Max_Size : Small_Positive) is private
+     with Default_Initial_Condition => Empty (Ring_Buffer_Type);
+
+   function Empty
+     (Buffer : in Ring_Buffer_Type) return Boolean;
+
+   function Full
+     (Buffer : in Ring_Buffer_Type) return Boolean;
+
+   function Size
+     (Buffer : in Ring_Buffer_Type) return Natural;
+
+   function Free
+     (Buffer : in Ring_Buffer_Type) return Natural;
+
+   function First
+     (Buffer : in Ring_Buffer_Type) return Element_Type
+   with
+     Pre => not Empty (Buffer);
+
+   function Last
+     (Buffer : in Ring_Buffer_Type) return Element_Type
+   with
+     Pre => not Empty (Buffer);
+
+   procedure Get
+     (Buffer   : in out Ring_Buffer_Type;
+      Element  :    out Element_Type)
+   with
+     Pre   => not Empty (Buffer) and
+              Size (Buffer) >= 1,
+     Post  => not Full (Buffer) and then
+              Element = First (Buffer'Old) and then
+              Size (Buffer) = Size (Buffer'Old) - 1;
+
+   procedure Put
+     (Buffer   : in out Ring_Buffer_Type;
+      Element  : in     Element_Type)
+   with
+     Pre   => not Full (Buffer),
+     Post  => not Empty (Buffer) and then
+              Last (Buffer) = Element and then
+              Size (Buffer) = Size (Buffer'Old) + 1;
+
+   procedure Clear
+     (Buffer : in out Ring_Buffer_Type)
+   with
+     Post => Empty (Buffer) and then
+             not Full (Buffer) and then
+             Size (Buffer) = 0;
+
+private
+   type Ring_Buffer_Type (Max_Size : Small_Positive) is record
+      Count : Small_Natural  := 0;
+      Head  : Small_Positive := 1;
+      Tail  : Small_Positive := Max_Size;
+      Items : Element_Array_Type (1 .. Max_Size);
+   end record
+     with Dynamic_Predicate =>
+       (Max_Size <= Small_Positive'Last and
+        Count    <= Max_Size and
+        Head     <= Max_Size and
+        Tail     <= Max_Size and
+        ((Count = 0 and Tail = Max_Size and Head = 1) or
+         (Count = Max_Size + Tail - Head + 1) or
+         (Count = Tail - Head + 1)));
+
+end Predicate8_Pkg;