r261410 - in /trunk/gcc: ada/ChangeLog ada/sem_...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Mon Jun 11 09:17:51 2018
New Revision: 261410

URL: https://gcc.gnu.org/viewcvs?rev=261410&root=gcc&view=rev
Log:
[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.

Added:
    trunk/gcc/testsuite/gnat.dg/contract1.adb
Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_util.adb
    trunk/gcc/testsuite/ChangeLog