]> git.ipfire.org Git - thirdparty/gcc.git/commit
[Ada] Fix handling of Loop_Entry for CodePeer/SPARK
authorpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Fri, 25 May 2018 09:03:34 +0000 (09:03 +0000)
committerpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Fri, 25 May 2018 09:03:34 +0000 (09:03 +0000)
commitac51778cd592f43ba8ef5e15217e92f172999678
tree53544bddf4d875bd0013449de2f154126f25f15b
parent230a45e9f27f7ea1e894147f65bf5e7a7a47dceb
[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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@260722 138bc75d-0d04-0410-961f-82ee72b054a4
gcc/ada/ChangeLog
gcc/ada/sem_prag.adb