From 1f233db3745890d8c9bed07f44a8b078bb2a0ee9 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 25 May 2018 09:03:34 +0000 Subject: [PATCH] [Ada] Fix handling of Loop_Entry for CodePeer/SPARK When the applicable Assertion_Policy is Ignore for a pragma containing an occurrence of attribute Loop_Entry, CodePeer and SPARK should still be able to analyze the corresponding pragma. GNAT frontend was wrongly translating X'Loop_Entry as X in the AST, as a side-effect of an optimization only valid for compilation and not for static analysis. This has no effect on compilation. 2018-05-25 Yannick Moy gcc/ada/ * sem_prag.adb (Check_Applicable_Policy): Deal specially with CodePeer and GNATprove modes when applicable policy is Ignore. From-SVN: r260722 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_prag.adb | 19 ++++++++++++++++--- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 838c445213c..a6fb3257cac 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-05-25 Yannick Moy + + * sem_prag.adb (Check_Applicable_Policy): Deal specially with CodePeer + and GNATprove modes when applicable policy is Ignore. + 2018-05-25 Eric Botcazou * freeze.adb (Freeze_Enumeration_Type): Do not give integer size to a diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 85a064d3ef2..eb6a018839b 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -28542,8 +28542,20 @@ package body Sem_Prag is when Name_Ignore | Name_Off => - Set_Is_Ignored (N, True); - Set_Is_Checked (N, False); + -- In CodePeer mode and GNATprove mode, we need to + -- consider all assertions, unless they are + -- disabled. Force Is_Checked on ignored assertions, in + -- particular because transformations of the AST may + -- depend on assertions being checked (e.g. the + -- translation of attribute 'Loop_Entry). + + if CodePeer_Mode or GNATprove_Mode then + Set_Is_Checked (N, True); + Set_Is_Ignored (N, False); + else + Set_Is_Ignored (N, True); + Set_Is_Checked (N, False); + end if; when Name_Check | Name_On @@ -28573,7 +28585,8 @@ package body Sem_Prag is -- If there are no specific entries that matched, then we let the -- setting of assertions govern. Note that this provides the needed -- compatibility with the RM for the cases of assertion, invariant, - -- precondition, predicate, and postcondition. + -- precondition, predicate, and postcondition. Note also that + -- Assertions_Enabled is forced in CodePeer mode and GNATprove mode. if Assertions_Enabled then Set_Is_Checked (N, True); -- 2.30.2