+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
-- 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 (
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,
+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
--- /dev/null
+-- { 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;
--- /dev/null
+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;
--- /dev/null
+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;
projects / gcc.git / commitdiff