[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 91a63bdc76d8d97e7e3a9d24264cc763d07e55ad..258c4ac5cc375688955f116e356040beb12d9388 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-05-30  Yannick Moy  <moy@adacore.com>
+
+       * sem_util.adb (Policy_In_Effect): Take into account CodePeer and
+       GNATprove modes.
+
 2018-05-30  Justin Squirek  <squirek@adacore.com>
 
        * libgnat/a-direct.adb, libgnat/a-direct.ads (Name_Case_Equivalence):

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index fd0864c77c022e58d43d70445d56715e01f73f6b..b629dbe8ae3875046debdee048aedb54f23ca1c2 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -22487,6 +22487,16 @@ package body Sem_Util is
          end if;
       end if;
 
+      --  In CodePeer mode and GNATprove mode, we need to consider all
+      --  assertions, unless they are disabled. Force Name_Check on
+      --  ignored assertions.
+
+      if Nam_In (Kind, Name_Ignore, Name_Off)
+        and then (CodePeer_Mode or GNATprove_Mode)
+      then
+         Kind := Name_Check;
+      end if;
+
       return Kind;
    end Policy_In_Effect;