This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Fix handling of Loop_Entry for CodePeer/SPARK
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Yannick Moy <moy at adacore dot com>
- Date: Fri, 25 May 2018 05:07:00 -0400
- Subject: [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.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
--- 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);