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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-06-11 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* sem_ch13.adb (Analyze_Aspect_Specifications): Don't split AND THEN
expressions in Pre/Post contracts while in GNATprove_Mode.--- gcc/ada/sem_ch13.adb
+++ 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
