[Ada] Add comment on special Heap variable used in GNATprove

gcc/ada/

	* spark_xrefs.ads: Add comment for Heap that it may remain
	Empty.

diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index 88a34c5b345e03803c27466ddff28c7a010892e8..ffd72685b27edf551d166698f9d42950ddb2d9fa 100644 (file)
--- a/gcc/ada/spark_xrefs.ads
+++ b/gcc/ada/spark_xrefs.ads
@@ -57,7 +57,8 @@ package SPARK_Xrefs is
    Heap : Entity_Id := Empty;
    --  A special entity which denotes the heap object; it should be considered
    --  constant, but needs to be variable, because it can only be initialized
-   --  after the node tables are created.
+   --  after the node tables are created. Also, it is only created if there is
+   --  an actual need for it, and remains Empty otherwise.
 
    -----------------
    -- Subprograms --