From 602c7bc2153591941a1f3c0edc4cb370910d2d95 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 10 Nov 2020 14:30:03 +0100 Subject: [Ada] Add comment on special Heap variable used in GNATprove gcc/ada/ * spark_xrefs.ads: Add comment for Heap that it may remain Empty. --- gcc/ada/spark_xrefs.ads | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'gcc/ada') diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index 88a34c5..ffd7268 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 -- -- cgit v1.1