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 chained locations in GNATprove for inherited pre and post

When a class-wide pre- or postcondition is inherited by an overriding
subprogram, the locations of the inherited pragma and of its expression
are the same as the locations of the original pragma. This is inconvenient
to distinguish properties proved on the overridden and the overriding
subprograms. This patch changes these locations to use chained locations
in such a case, similarly to what we get on generic instantiations and
inlined subprograms.

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

2016-07-04  Yannick Moy  <>

	* sem_ch12.adb, Update calls to
	Create_Instantiation_Source to use default argument.
	(Adjust_Inherited_Pragma_Sloc): New function to adjust sloc
	of inherited pragma.
	New function that wraps call to Create_Instantiation_Source for
	copying an inherited pragma.
	(Set_Copied_Sloc_For_Inlined_Body): Update call to
	Create_Instantiation_Source with new arguments.
	* sem_prag.adb (Build_Pragma_Check_Equivalent): In the case
	of inherited pragmas, use the generic machinery to get chained
	locations for the pragma and its sub-expressions.
	* sinput-c.adb: Adapt to new type Source_File_Record.
	* sinput-l.adb, (Create_Instantiation_Source):
	Add parameter Inherited_Pragma and make parameter Inlined_Body
	* sinput.adb, (Comes_From_Inherited_Pragma): New
	function to return when a location comes from an inherited pragma.
	(Inherited_Pragma): New function to detect when a location comes
	from an inherited pragma.
	(Source_File_Record): New component Inherited_Pragma.

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]