This patch fixes a compiler abort on a precondition whose condition
includes a quantified expression.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-08-14 Ed Schonberg <schonb...@adacore.com>
gcc/ada/
* 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.
gcc/testsuite/
* gnat.dg/predicate12.adb, gnat.dg/predicate12.ads: New
testcase.--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -20799,16 +20799,27 @@ package body Sem_Util is
-- 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
@@ -21081,7 +21092,14 @@ package body Sem_Util is
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
@@ -21225,6 +21243,12 @@ package body Sem_Util is
-- * 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.
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/predicate12.adb
@@ -0,0 +1,6 @@
+-- { dg-do compile }
+-- { dg-options "-gnata" }
+
+package body Predicate12 is
+ procedure Dummy is null;
+end Predicate12;
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/predicate12.ads
@@ -0,0 +1,42 @@
+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;
