[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  <trojanek@adacore.com>

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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b8a5ea4cbec61919d47d86760cadedbbf84f91d3..f35a232fc7c2ea960c895785aaf7f565315cca80 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-06-11  Piotr Trojanek  <trojanek@adacore.com>
+
+       * sem_util.adb (Is_Potentially_Unevaluated): Fix detection of contracts
+       with AND THEN expressions broken down into individual conjuncts.
+
 2018-06-11  Ed Schonberg  <schonberg@adacore.com>
 
        * exp_ch7.adb (Check_Unnesting_Elaboration_Code): Add guard.

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 69934f018ca735c0f235a1cccb5a1b1c27d515f4..ec2640946412eddaaec6e4482880262b4df8812c 100644 (file)
--- 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 0b16f0ccac4b9a302be6da942c0522acb36473b9..a34c710adbc81b172d14282ab564f73c1e7132aa 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2018-06-11  Piotr Trojanek  <trojanek@adacore.com>
+
+       * gnat.dg/contract1.adb: New testcase.
+
 2018-06-11  Javier Miranda  <miranda@adacore.com>
 
        * 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 (file)
index 0000000..286fbc5
--- /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;