This is the mail archive of the 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] Use Is_Inlined flag to mark fully inlined subp in GNATprove mode

In GNATprove mode, some subprograms may be partially inlined, due to
recursion, or because some calls are in a potentially unevaluated context,
which would lead to code that GNATprove would not be able to handle. In
those cases, the body-to-inline has been built, and potentially already be
inlined. Hence, the separate flag Is_Inlined is used to convey the
information that not all calls have been inlined, by setting it to False.
GNATprove uses this information to decide which subprograms to analyze.

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

2014-07-30  Yannick Moy  <>

	* (Is_Inlined): Document new use in GNATprove mode.
	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add comments
	to explain rationale for inlining or not in GNATprove mode.
	(Expand_Inlined_Call): In GNATprove mode, set Is_Inlined flag
	to False when inlining is not possible.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Set Is_Inlined
	flag to indicate that subprogram is fully inlined. To be reversed
	if inlining problem is found.
	* sem_res.adb (Resolve_Call): Set Is_Inlined flag to False when
	call in potentially unevaluated context.

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]