diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2018-06-11 09:17:56 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-06-11 09:17:56 +0000 |
| commit | 270c6b4d6f9300f36cb7e06594d71a62ab59af0a (patch) | |
| tree | 6d417c6a4c0ef588c9135a3fb625a2a35b9d6f52 | |
| parent | f062a9757ac2d2cf368f1a0d82fedac54ca365fb (diff) | |
| download | gcc-270c6b4d6f9300f36cb7e06594d71a62ab59af0a.zip gcc-270c6b4d6f9300f36cb7e06594d71a62ab59af0a.tar.gz gcc-270c6b4d6f9300f36cb7e06594d71a62ab59af0a.tar.bz2 | |
[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
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 8 |
2 files changed, 11 insertions, 2 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f35a232..00af9be 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 2018-06-11 Piotr Trojanek <trojanek@adacore.com> + * sem_ch13.adb (Analyze_Aspect_Specifications): Don't split AND THEN + expressions in Pre/Post contracts while in GNATprove_Mode. + +2018-06-11 Piotr Trojanek <trojanek@adacore.com> + * sem_util.adb (Is_Potentially_Unevaluated): Fix detection of contracts with AND THEN expressions broken down into individual conjuncts. diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 145f637..efa2709 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -3443,9 +3443,13 @@ package body Sem_Ch13 is -- We do not do this in ASIS mode, as ASIS relies on the -- original node representing the complete expression, when - -- retrieving it through the source aspect table. + -- retrieving it through the source aspect table. Also, we + -- don't do this in GNATprove mode, because it brings no + -- benefit for proof and causes annoynace for flow analysis, + -- which prefers to be as close to the original source code + -- as possible. - if not ASIS_Mode + if not (ASIS_Mode or GNATprove_Mode) and then (Pname = Name_Postcondition or else not Class_Present (Aspect)) then |