r261411 - in /trunk/gcc/ada: ChangeLog sem_ch13...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Mon Jun 11 09:17:56 2018
New Revision: 261411

URL: https://gcc.gnu.org/viewcvs?rev=261411&root=gcc&view=rev
Log:
[Ada] Don't split AND THEN expressions in GNATprove_Mode

Splitting AND THEN expressions in contracts into separate pragma Check
is only useful for compilation when the error message points to a failed
conjunct. For proof it is of no use; for flow analysis it is annoying.
Also, it makes debugging harder. Now it is disabled in GNATprove_Mode.

Compilation is not affected, so no test provided.

2018-06-11  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* sem_ch13.adb (Analyze_Aspect_Specifications): Don't split AND THEN
	expressions in Pre/Post contracts while in GNATprove_Mode.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_ch13.adb