diff mbox series

[Ada] Fix handling of Pre/Post contracts with AND THEN expressions

Message ID 20180611092204.GA134873@adacore.com
State New
Headers show
Series [Ada] Fix handling of Pre/Post contracts with AND THEN expressions | expand

Commit Message

Pierre-Marie de Rodat June 11, 2018, 9:22 a.m. UTC 
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)

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
diff mbox series

Patch

--- gcc/ada/sem_util.adb
+++ 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;
 

--- /dev/null
new file mode 100644
+++ 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;