contract1.adb
351 Bytes
-
[Ada] Fix handling of Pre/Post contracts with AND THEN expressions · f062a975
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
Piotr Trojanek committed