[Ada] Avoid spurious warning on assertions with Loop_Entry

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.

2019-07-11  Yannick Moy  <moy@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.

From-SVN: r273403

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 95c898b3768d0163ec73cd776df841294f936a6e..15b90e379cbfb6b42921d18b98c577bcac2d18c7 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-07-11  Yannick Moy  <moy@adacore.com>
+
+       * sem_eval.adb (Is_Same_Value): Add special case for rewritten
+       Loop_Entry attribute.
+
 2019-07-11  Claire Dross  <dross@adacore.com>
 
        * gnat1drv.adb: SPARK checking rules for pointer aliasing are

diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
index e140fa72ffbdc91fcc92d89867160789393576b1..734c961fe620561700dc7eaa2e8eb798d632a509 100644 (file)
--- a/gcc/ada/sem_eval.adb
+++ b/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)

diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog
index baef966cb2d63043c78d1af7f39824bb9cea4f63..f4a6d05f7c098746212836723ba9e92b82a45ddb 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2019-07-11  Yannick Moy  <moy@adacore.com>
+
+       * gnat.dg/loop_entry1.adb: New testcase.
+
 2019-07-11  Ed Schonberg  <schonberg@adacore.com>
 
        * gnat.dg/prot8.adb, gnat.dg/prot8.ads: New testcase.

diff --git a/gcc/testsuite/gnat.dg/loop_entry1.adb b/gcc/testsuite/gnat.dg/loop_entry1.adb
new file mode 100644 (file)
index 0000000..39cb8d0
--- /dev/null
+++ b/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;