[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