r260943 - in /trunk/gcc/ada: ChangeLog sem_util...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Wed May 30 08:58:17 2018
New Revision: 260943

URL: https://gcc.gnu.org/viewcvs?rev=260943&root=gcc&view=rev
Log:
[Ada] Correctly ignore Assertion_Policy in modes CodePeer and GNATprove

In the modes for static analysis with CodePeer or formal verification with
GNATprove, the value of Assertion_Policy for a given policy is ignored if
it's not Disable, as CodePeer/GNATprove are meant to check assertions even
when not enabled at run time. This was not done consistently, which could
lead to spurious errors on policy mismatch on ghost code inside assertions.

There is no impact on compilation.

2018-05-30  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_util.adb (Policy_In_Effect): Take into account CodePeer and
	GNATprove modes.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_util.adb