This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Selectively inline subprograms in GNATprove mode


For formal verification with GNATprove, frontend inlining can be used to
relieve users from the need to add contracts to local subprograms. Thus,
we adopt here a simple policy for inlining in GNATprove mode, which consists
in inlining all local subprograms which can be inlined, as soon as they
don't have a contract. This policy gives to the user the control over which
subprograms may be inlined.

This is under debug flag -gnatdQ for now, until remaining issues have been
fixed.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]