[Ada] Fix handling of separate units in GNATprove cross references

[Arnaud Charlet <charlet at adacore dot com>]

The collect of cross references for computing effects of subprograms
in GNATprove was done incorrectly in the case of separate units. This is
now fixed, by bypassing subunits when computing the unit of interest for
both scopes and cross references.

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

2016-06-14  Yannick Moy  <moy@adacore.com>

	* lib-xref-spark_specific.adb (Add_SPARK_File): Do not traverse
	subunits directly, as they are already traversed as part of the
	top-level unit to which they belong.
	(Add_SPARK_Xrefs): Add assertions to ensure correct sorting.
	(Generate_Dereference): Use unique definition place for special
	variable __HEAP, to ensure correct sorting of references.
	* lib-xref.adb (Generate_Reference): Use top-level unit in case
	of subunits.
	* lib.adb, lib.ads (Get_Top_Level_Code_Unit): New functions that
	compute the top-level code unit for a source location of AST node,
	that go past subunits.

Attachment: difs
Description: Text document