From: Yannick Moy <moy@adacore.com>
Date: Tue, 10 Nov 2020 13:30:03 +0000 (+0100)
Subject: [Ada] Add comment on special Heap variable used in GNATprove
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=602c7bc2153591941a1f3c0edc4cb370910d2d95;p=gcc.git

[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 88a34c5b345..ffd72685b27 100644
--- 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 --