[Ada] Don't split AND THEN expressions in GNATprove_Mode
authorPiotr Trojanek <trojanek@adacore.com>
Mon, 11 Jun 2018 09:17:56 +0000 (09:17 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 11 Jun 2018 09:17:56 +0000 (09:17 +0000)
commit270c6b4d6f9300f36cb7e06594d71a62ab59af0a
tree6d417c6a4c0ef588c9135a3fb625a2a35b9d6f52
parentf062a9757ac2d2cf368f1a0d82fedac54ca365fb
[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.

From-SVN: r261411
gcc/ada/ChangeLog
gcc/ada/sem_ch13.adb