+2019-08-14 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_util.adb (New_Copy_Tree, Visit_Entity): A quantified
+ expression includes the implicit declaration of the loop
+ parameter. When a quantified expression is copied during
+ expansion, for example when building the precondition code from
+ the generated pragma, a new loop parameter must be created for
+ the new tree, to prevent duplicate declarations for the same
+ symbol.
+
2019-08-14 Yannick Moy <moy@adacore.com>
* sem_disp.adb (Check_Dispatching_Operation): Update assertion
-- this restriction leads to a performance penalty.
-- ??? this list is flaky, and may hide dormant bugs
+ -- Should functions be included???
+
+ -- Loop parameters appear within quantified expressions and contain
+ -- an entity declaration that must be replaced when the expander is
+ -- active if the expression has been preanalyzed or analyzed.
elsif not Ekind_In (Id, E_Block,
E_Constant,
E_Label,
+ E_Loop_Parameter,
E_Procedure,
E_Variable)
and then not Is_Type (Id)
then
return;
+ elsif Ekind (Id) = E_Loop_Parameter
+ and then No (Etype (Condition (Parent (Parent (Id)))))
+ then
+ return;
+
-- Nothing to do when the entity was already visited
elsif NCT_Tables_In_Use
begin
pragma Assert (Nkind (N) not in N_Entity);
- if Nkind (N) = N_Expression_With_Actions then
+ -- If the node is a quantified expression and expander is active,
+ -- it contains an implicit declaration that may require a new entity
+ -- when the condition has already been (pre)analyzed.
+
+ if Nkind (N) = N_Expression_With_Actions
+ or else
+ (Nkind (N) = N_Quantified_Expression and then Expander_Active)
+ then
EWA_Level := EWA_Level + 1;
elsif EWA_Level > 0
-- * Semantic fields of nodes such as First_Real_Statement must be
-- updated to reference the proper replicated nodes.
+ -- Finally, quantified expressions contain an implicit delaration for
+ -- the bound variable. Given that quantified expressions appearing
+ -- in contracts are copied to create pragmas and eventually checking
+ -- procedures, a new bound variable must be created for each copy, to
+ -- prevent multiple declarations of the same symbol.
+
-- To meet all these demands, routine New_Copy_Tree is split into two
-- phases.
+2019-08-14 Ed Schonberg <schonberg@adacore.com>
+
+ * gnat.dg/predicate12.adb, gnat.dg/predicate12.ads: New
+ testcase.
+
2019-08-14 Gary Dismukes <dismukes@adacore.com>
* gnat.dg/task5.adb: New testcase.
--- /dev/null
+-- { dg-do compile }
+-- { dg-options "-gnata" }
+
+package body Predicate12 is
+ procedure Dummy is null;
+end Predicate12;
--- /dev/null
+package Predicate12 is
+
+ subtype Index_Type is Positive range 1 .. 100;
+ type Array_Type is array(Index_Type) of Integer;
+
+ type Search_Engine is interface;
+
+ procedure Search
+ (S : in Search_Engine;
+ Search_Item : in Integer;
+ Items : in Array_Type;
+ Found : out Boolean;
+ Result : out Index_Type) is abstract
+ with
+ Pre'Class =>
+ (for all J in Items'Range =>
+ (for all K in J + 1 .. Items'Last => Items(J) <= Items(K))),
+ Post'Class =>
+ (if Found then Search_Item = Items(Result)
+ else (for all J in Items'Range => Items(J) /= Search_Item));
+
+ type Binary_Search_Engine is new Search_Engine with null record;
+
+ procedure Search
+ (S : in Binary_Search_Engine;
+ Search_Item : in Integer;
+ Items : in Array_Type;
+ Found : out Boolean;
+ Result : out Index_Type) is null;
+
+ type Forward_Search_Engine is new Search_Engine with null record;
+
+ procedure Search
+ (S : in Forward_Search_Engine;
+ Search_Item : in Integer;
+ Items : in Array_Type;
+ Found : out Boolean;
+ Result : out Index_Type) is null;
+
+ procedure Dummy;
+
+end Predicate12;