[Ada] Correctly ignore Assertion_Policy in modes CodePeer and GNATprove
authorYannick Moy <moy@adacore.com>
Wed, 30 May 2018 08:58:17 +0000 (08:58 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Wed, 30 May 2018 08:58:17 +0000 (08:58 +0000)
commitf2a3c2fa828ced9f08597def430b3149ff9a4961
treedff76c55c12e1f6c6799455a702662f10746d54e
parentefa760f0ca2f45209525de0e9b6939351e1a0072
[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.

From-SVN: r260943
gcc/ada/ChangeLog
gcc/ada/sem_util.adb