diff options
| author | Yannick Moy <moy@adacore.com> | 2020-11-10 14:30:03 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-11-30 09:16:17 -0500 |
| commit | 602c7bc2153591941a1f3c0edc4cb370910d2d95 (patch) | |
| tree | a81f967364d5a4eae68dc72156a0dddcc3b97661 /gcc/ada/spark_xrefs.ads | |
| parent | 50a2820f9d422cc59d6674d7f775b921cad44bfb (diff) | |
| download | gcc-602c7bc2153591941a1f3c0edc4cb370910d2d95.zip gcc-602c7bc2153591941a1f3c0edc4cb370910d2d95.tar.gz gcc-602c7bc2153591941a1f3c0edc4cb370910d2d95.tar.bz2 | |
[Ada] Add comment on special Heap variable used in GNATprove
gcc/ada/
* spark_xrefs.ads: Add comment for Heap that it may remain
Empty.
Diffstat (limited to 'gcc/ada/spark_xrefs.ads')
| -rw-r--r-- | gcc/ada/spark_xrefs.ads | 3 |
1 files changed, 2 insertions, 1 deletions
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 -- |