From 708fb956d9b625c150aadf9fb6394651ef054b5a Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 11 Jul 2019 08:03:14 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 5 +++ gcc/ada/sem_eval.adb | 49 +++++++++++++++++++++------ gcc/testsuite/ChangeLog | 4 +++ gcc/testsuite/gnat.dg/loop_entry1.adb | 13 +++++++ 4 files changed, 61 insertions(+), 10 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/loop_entry1.adb diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 95c898b3768..15b90e379cb 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-11 Yannick Moy + + * sem_eval.adb (Is_Same_Value): Add special case for rewritten + Loop_Entry attribute. + 2019-07-11 Claire Dross * gnat1drv.adb: SPARK checking rules for pointer aliasing are diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb index e140fa72ffb..734c961fe62 100644 --- 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 baef966cb2d..f4a6d05f7c0 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2019-07-11 Yannick Moy + + * gnat.dg/loop_entry1.adb: New testcase. + 2019-07-11 Ed Schonberg * 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 index 00000000000..39cb8d03ecb --- /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; -- 2.30.2