From f062a9757ac2d2cf368f1a0d82fedac54ca365fb Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Mon, 11 Jun 2018 09:17:51 +0000 Subject: [PATCH] [Ada] Fix handling of Pre/Post contracts with AND THEN expressions Pre- and postconditions with top-level AND THEN expressions are broken down into checks of indivudial conjuncts for more precise error reporting. This rewrite interfers with detection of potentially unevaluadted use of 'Old, e.g. a contract like "Pre => Foo and then Bar" is rewritten into a two pragmas Check, for expressions "Foo" and "Bar", but the latter remains potentially unevaluted. This patch fixes detection of the AND THEN rewrite. This fixes inlining in the GNATprove mode, i.e. the following testc case must not emit a warning like: contract1.adb:14:07: info: no contextual analysis of "Foo" (in potentially unevaluated context) 2018-06-11 Piotr Trojanek gcc/ada/ * sem_util.adb (Is_Potentially_Unevaluated): Fix detection of contracts with AND THEN expressions broken down into individual conjuncts. gcc/testsuite/ * gnat.dg/contract1.adb: New testcase. From-SVN: r261410 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_util.adb | 4 +++- gcc/testsuite/ChangeLog | 4 ++++ gcc/testsuite/gnat.dg/contract1.adb | 20 ++++++++++++++++++++ 4 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 gcc/testsuite/gnat.dg/contract1.adb diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b8a5ea4cbec..f35a232fc7c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-06-11 Piotr Trojanek + + * sem_util.adb (Is_Potentially_Unevaluated): Fix detection of contracts + with AND THEN expressions broken down into individual conjuncts. + 2018-06-11 Ed Schonberg * exp_ch7.adb (Check_Unnesting_Elaboration_Code): Add guard. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 69934f018ca..ec264094641 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -16453,7 +16453,9 @@ package body Sem_Util is while Present (Par) and then Nkind (Par) /= N_Pragma_Argument_Association loop - if Nkind (Original_Node (Par)) = N_And_Then then + if Is_Rewrite_Substitution (Par) + and then Nkind (Original_Node (Par)) = N_And_Then + then return True; end if; diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 0b16f0ccac4..a34c710adbc 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2018-06-11 Piotr Trojanek + + * gnat.dg/contract1.adb: New testcase. + 2018-06-11 Javier Miranda * gnat.dg/aggr23.adb, gnat.dg/aggr23_q.adb, gnat.dg/aggr23_tt.ads: New diff --git a/gcc/testsuite/gnat.dg/contract1.adb b/gcc/testsuite/gnat.dg/contract1.adb new file mode 100644 index 00000000000..286fbc557ca --- /dev/null +++ b/gcc/testsuite/gnat.dg/contract1.adb @@ -0,0 +1,20 @@ +-- { dg-do compile } +-- { dg-options "-gnatd.F -gnatwa" } + +with Ada.Dispatching; + +procedure Contract1 with SPARK_Mode is + + function Foo return Boolean is + begin + Ada.Dispatching.Yield; + return True; + end Foo; + + Dummy : constant Integer := 0; + +begin + if Foo and then True then + raise Program_Error; + end if; +end Contract1; -- 2.30.2