[Ada] Fix handling of Loop_Entry for CodePeer/SPARK
authorYannick Moy <moy@adacore.com>
Fri, 25 May 2018 09:03:34 +0000 (09:03 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Fri, 25 May 2018 09:03:34 +0000 (09:03 +0000)
commit1f233db3745890d8c9bed07f44a8b078bb2a0ee9
tree53544bddf4d875bd0013449de2f154126f25f15b
parent0d0cd28165d05981eadc966224dca77b87111b62
[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
gcc/ada/ChangeLog
gcc/ada/sem_prag.adb