From: Piotr Trojanek <[email protected]>
Cross-references are used by GNATprove for code that is not in SPARK. They are
sorted using an auxiliary array. This array should be allocated on the heap and
not on stack, because it can be arbitrarily large, especially for
auto-generated code.
gcc/ada/ChangeLog:
* lib-xref.adb (Output_References): Put local array object on the heap.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/lib-xref.adb | 14 +++++++++++++-
1 file changed, 13 insertions(+), 1 deletion(-)
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index aa9ae57f60e..d7dc7178daa 100644
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -23,6 +23,7 @@
-- --
------------------------------------------------------------------------------
+with Ada.Unchecked_Deallocation;
with Atree; use Atree;
with Csets; use Csets;
with Einfo; use Einfo;
@@ -1827,7 +1828,16 @@ package body Lib.Xref is
Nrefs : constant Nat := Xrefs.Last;
-- Number of references in table
- Rnums : array (0 .. Nrefs) of Nat;
+ type Refs_Numbers is array (0 .. Nrefs) of Nat;
+ type Refs_Numbers_Ptr is access Refs_Numbers;
+ -- Since the number of references can be large, we need to allocate
+ -- the sorting array on the heap.
+
+ procedure Free is
+ new Ada.Unchecked_Deallocation (Refs_Numbers, Refs_Numbers_Ptr);
+ -- Release memory allocated for the sorting array
+
+ Rnums : Refs_Numbers_Ptr := new Refs_Numbers;
-- This array contains numbers of references in the Xrefs table.
-- This list is sorted in output order. The extra 0'th entry is
-- convenient for the call to sort. When we sort the table, we
@@ -2709,6 +2719,8 @@ package body Lib.Xref is
null;
end loop;
+ Free (Rnums);
+
Write_Info_EOL;
end Output_Refs;
end Output_References;
--
2.51.0
