From e87f67eb5d8671bc7c98dbf10106fda34114b293 Mon Sep 17 00:00:00 2001 From: Ed Schonberg Date: Mon, 8 Jul 2019 08:12:46 +0000 Subject: [PATCH] [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 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 | 9 +++ gcc/ada/sem_ch13.adb | 18 +++++- gcc/testsuite/ChangeLog | 5 ++ gcc/testsuite/gnat.dg/predicate8.adb | 15 +++++ gcc/testsuite/gnat.dg/predicate8_pkg.adb | 64 +++++++++++++++++++ gcc/testsuite/gnat.dg/predicate8_pkg.ads | 81 ++++++++++++++++++++++++ 6 files changed, 189 insertions(+), 3 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/predicate8.adb create mode 100644 gcc/testsuite/gnat.dg/predicate8_pkg.adb create mode 100644 gcc/testsuite/gnat.dg/predicate8_pkg.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8a729d1e1a5..687c4abefae 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,12 @@ +2019-07-08 Ed Schonberg + + * 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 * checks.adb (Apply_Accessibility_Check): Add logic to fetch the diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 4c743666b23..b62e2971def 100644 --- a/gcc/ada/sem_ch13.adb +++ b/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, diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index db493b33cf5..a5a44a557a7 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,8 @@ +2019-07-08 Ed Schonberg + + * gnat.dg/predicate8.adb, gnat.dg/predicate8_pkg.adb, + gnat.dg/predicate8_pkg.ads: New testcase. + 2019-07-08 Richard Biener PR tree-optimization/83518 diff --git a/gcc/testsuite/gnat.dg/predicate8.adb b/gcc/testsuite/gnat.dg/predicate8.adb new file mode 100644 index 00000000000..00196996afa --- /dev/null +++ b/gcc/testsuite/gnat.dg/predicate8.adb @@ -0,0 +1,15 @@ +-- { 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; diff --git a/gcc/testsuite/gnat.dg/predicate8_pkg.adb b/gcc/testsuite/gnat.dg/predicate8_pkg.adb new file mode 100644 index 00000000000..20626d94393 --- /dev/null +++ b/gcc/testsuite/gnat.dg/predicate8_pkg.adb @@ -0,0 +1,64 @@ +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; diff --git a/gcc/testsuite/gnat.dg/predicate8_pkg.ads b/gcc/testsuite/gnat.dg/predicate8_pkg.ads new file mode 100644 index 00000000000..fd25294ea38 --- /dev/null +++ b/gcc/testsuite/gnat.dg/predicate8_pkg.ads @@ -0,0 +1,81 @@ +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; -- 2.30.2