[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f35a232..00af9be 100644 (file)
--- 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 (file)
--- 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