[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  <moy@adacore.com>

gcc/ada/

	* sem_prag.adb (Check_Applicable_Policy): Deal specially with CodePeer
	and GNATprove modes when applicable policy is Ignore.

From-SVN: r260722

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 838c445213c7fa068f1d7f30281a2ce4d9aebb4b..a6fb3257cacd48c4a6c072adc95e68eb0b785d4f 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-05-25  Yannick Moy  <moy@adacore.com>
+
+       * sem_prag.adb (Check_Applicable_Policy): Deal specially with CodePeer
+       and GNATprove modes when applicable policy is Ignore.
+
 2018-05-25  Eric Botcazou  <ebotcazou@adacore.com>
 
        * 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 85a064d3ef2a79a0f40d2f3addbe1d98fa58c766..eb6a018839b1f1c452350b2cd21968119104a152 100644 (file)
--- 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);