From f2a3c2fa828ced9f08597def430b3149ff9a4961 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 30 May 2018 08:58:17 +0000 Subject: [PATCH] [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 gcc/ada/ * sem_util.adb (Policy_In_Effect): Take into account CodePeer and GNATprove modes. From-SVN: r260943 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_util.adb | 10 ++++++++++ 2 files changed, 15 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 91a63bdc76d..258c4ac5cc3 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-05-30 Yannick Moy + + * sem_util.adb (Policy_In_Effect): Take into account CodePeer and + GNATprove modes. + 2018-05-30 Justin Squirek * 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 fd0864c77c0..b629dbe8ae3 100644 --- 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;