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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-05-25 Yannick Moy <m...@adacore.com>
gcc/ada/
* sem_prag.adb (Check_Applicable_Policy): Deal specially with CodePeer
and GNATprove modes when applicable policy is Ignore.--- gcc/ada/sem_prag.adb
+++ 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);
