OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Correctly ignore Assertion_Policy in modes CodePeer and GNATprove

Browse Source 
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
This commit is contained in:
Yannick Moy 2018-05-30 08:58:17 +00:00 committed by Pierre-Marie de Rodat
parent efa760f0ca
commit f2a3c2fa82
2 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
gcc/ada/ChangeLog
View File

@ -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> 2018-05-30 Justin Squirek <squirek@adacore.com>
* libgnat/a-direct.adb, libgnat/a-direct.ads (Name_Case_Equivalence): * libgnat/a-direct.adb, libgnat/a-direct.ads (Name_Case_Equivalence):

10
gcc/ada/sem_util.adb
View File

@ -22487,6 +22487,16 @@ package body Sem_Util is
end if; end if;
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; return Kind;
end Policy_In_Effect; end Policy_In_Effect;