This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Correctly ignore Assertion_Policy in modes CodePeer and GNATprove
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Yannick Moy <moy at adacore dot com>
- Date: Wed, 30 May 2018 05:00:40 -0400
- Subject: [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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-05-30 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_util.adb (Policy_In_Effect): Take into account CodePeer and
GNATprove modes.
--- gcc/ada/sem_util.adb
+++ 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;