r260722 - in /trunk/gcc/ada: ChangeLog sem_prag...

pmderodat@gcc.gnu.org pmderodat@gcc.gnu.org
Fri May 25 09:03:00 GMT 2018


Author: pmderodat
Date: Fri May 25 09:03:34 2018
New Revision: 260722

URL: https://gcc.gnu.org/viewcvs?rev=260722&root=gcc&view=rev
Log:
[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.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_prag.adb



More information about the Gcc-cvs mailing list