[Ada] Fix handling of Pre/Post contracts with AND THEN expressions
authorPiotr Trojanek <trojanek@adacore.com>
Mon, 11 Jun 2018 09:17:51 +0000 (09:17 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 11 Jun 2018 09:17:51 +0000 (09:17 +0000)
commitf062a9757ac2d2cf368f1a0d82fedac54ca365fb
tree4271aca4b3aa089d1fb1f075ec3f762399afdc78
parentacc257bbf0fe5cc6560d8fe1607d1be64528a96f
[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
gcc/ada/ChangeLog
gcc/ada/sem_util.adb
gcc/testsuite/ChangeLog
gcc/testsuite/gnat.dg/contract1.adb [new file with mode: 0644]