r213205 - in /trunk/gcc/ada: ChangeLog debug.ad...

[charlet@gcc.gnu.org]

Author: charlet
Date: Tue Jul 29 14:55:24 2014
New Revision: 213205

URL: https://gcc.gnu.org/viewcvs?rev=213205&root=gcc&view=rev
Log:
2014-07-29  Yannick Moy  <moy@adacore.com>

	* debug.adb Enable GNATprove inlining under debug flag -gnatdQ for now.
	* inline.ads, inline.adb (Can_Be_Inlined_In_GNATprove_Mode): New
	function to decide when a subprogram can be inlined in GNATprove mode.
	(Check_And_Build_Body_To_Inline): Include GNATprove_Mode as a
	condition for possible inlining.
	* sem_ch10.adb (Analyze_Compilation_Unit): Remove special case
	for Inline_Always in GNATprove mode.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build inlined
	body for subprograms in GNATprove mode, under debug flag -gnatdQ.
	* sem_prag.adb Minor change in comments.
	* sem_res.adb (Resolve_Call): Only perform GNATprove inlining
	inside subprograms marked as SPARK_Mode On.
	* sinfo.ads: Minor typo fix.


Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/debug.adb
    trunk/gcc/ada/inline.adb
    trunk/gcc/ada/inline.ads
    trunk/gcc/ada/sem_ch10.adb
    trunk/gcc/ada/sem_ch6.adb
    trunk/gcc/ada/sem_prag.adb
    trunk/gcc/ada/sem_res.adb
    trunk/gcc/ada/sinfo.ads