| commit | 270c6b4d6f9300f36cb7e06594d71a62ab59af0a | |
| author | Piotr Trojanek <trojanek@adacore.com> | |
| Mon, 11 Jun 2018 09:17:56 +0000 (11 09:17 +0000) | ||
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | |
| Mon, 11 Jun 2018 09:17:56 +0000 (11 09:17 +0000) | ||
| tree | 6d417c6a4c0ef588c9135a3fb625a2a35b9d6f52 | treesnapshot (tar.gz zip) |
| parent | f062a9757ac2d2cf368f1a0d82fedac54ca365fb | commitdiff |
[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
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 | diffblobblamehistory | |
| gcc/ada/sem_ch13.adb | diffblobblamehistory |