When the Loop_Entry attribute is used inside a loop invariant or another
assertion where it is allowed, it may lead to spurious warnings on
conditions that are detected to be always valid. Now fixed.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-11 Yannick Moy <m...@adacore.com>
gcc/ada/
* sem_eval.adb (Is_Same_Value): Add special case for rewritten
Loop_Entry attribute.
gcc/testsuite/
* gnat.dg/loop_entry1.adb: New testcase.--- gcc/ada/sem_eval.adb
+++ gcc/ada/sem_eval.adb
@@ -986,6 +986,13 @@ package body Sem_Eval is
Lf : constant Node_Id := Compare_Fixup (L);
Rf : constant Node_Id := Compare_Fixup (R);
+ function Is_Rewritten_Loop_Entry (N : Node_Id) return Boolean;
+ -- An attribute reference to Loop_Entry may have been rewritten into
+ -- its prefix as a way to avoid generating a constant for that
+ -- attribute when the corresponding pragma is ignored. These nodes
+ -- should be ignored when deciding if they can be equal to one
+ -- another.
+
function Is_Same_Subscript (L, R : List_Id) return Boolean;
-- L, R are the Expressions values from two attribute nodes for First
-- or Last attributes. Either may be set to No_List if no expressions
@@ -993,6 +1000,19 @@ package body Sem_Eval is
-- expressions represent the same subscript (note one case is where
-- one subscript is missing and the other is explicitly set to 1).
+ -----------------------------
+ -- Is_Rewritten_Loop_Entry --
+ -----------------------------
+
+ function Is_Rewritten_Loop_Entry (N : Node_Id) return Boolean is
+ Orig_N : constant Node_Id := Original_Node (N);
+ begin
+ return Orig_N /= N
+ and then Nkind (Orig_N) = N_Attribute_Reference
+ and then Get_Attribute_Id (Attribute_Name (Orig_N)) =
+ Attribute_Loop_Entry;
+ end Is_Rewritten_Loop_Entry;
+
-----------------------
-- Is_Same_Subscript --
-----------------------
@@ -1018,23 +1038,32 @@ package body Sem_Eval is
-- Start of processing for Is_Same_Value
begin
- -- Values are the same if they refer to the same entity and the
- -- entity is non-volatile. This does not however apply to Float
- -- types, since we may have two NaN values and they should never
- -- compare equal.
+ -- Loop_Entry nodes rewritten into their prefix inside ignored
+ -- pragmas should never lead to a decision of equality.
- -- If the entity is a discriminant, the two expressions may be bounds
- -- of components of objects of the same discriminated type. The
- -- values of the discriminants are not static, and therefore the
- -- result is unknown.
+ if Is_Rewritten_Loop_Entry (Lf)
+ or else Is_Rewritten_Loop_Entry (Rf)
+ then
+ return False;
- -- It would be better to comment individual branches of this test ???
+ -- Values are the same if they refer to the same entity and the
+ -- entity is nonvolatile.
- if Nkind_In (Lf, N_Identifier, N_Expanded_Name)
+ elsif Nkind_In (Lf, N_Identifier, N_Expanded_Name)
and then Nkind_In (Rf, N_Identifier, N_Expanded_Name)
and then Entity (Lf) = Entity (Rf)
+
+ -- If the entity is a discriminant, the two expressions may be
+ -- bounds of components of objects of the same discriminated type.
+ -- The values of the discriminants are not static, and therefore
+ -- the result is unknown.
+
and then Ekind (Entity (Lf)) /= E_Discriminant
and then Present (Entity (Lf))
+
+ -- This does not however apply to Float types, since we may have
+ -- two NaN values and they should never compare equal.
+
and then not Is_Floating_Point_Type (Etype (L))
and then not Is_Volatile_Reference (L)
and then not Is_Volatile_Reference (R)
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/loop_entry1.adb
@@ -0,0 +1,13 @@
+-- { dg-do compile }
+-- { dg-options "-gnatwc" }
+
+procedure Loop_Entry1 (X, Y : in out Integer) is
+begin
+ while X < Y loop
+ pragma Loop_Invariant
+ (X >= X'Loop_Entry and then Y <= Y'Loop_Entry);
+
+ X := X + 1;
+ Y := Y - 1;
+ end loop;
+end Loop_Entry1;
