1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S P A R K _ X R E F S --
-- --
-- S p e c --
-- --
-- Copyright (C) 2011-2024, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
-- for more details. You should have received a copy of the GNU General --
-- Public License distributed with GNAT; see file COPYING3. If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
-- This package defines data structures used to expose frontend
-- cross-references to the SPARK backend.
with Types; use Types;
package SPARK_Xrefs is
type SPARK_Xref_Record is record
Entity : Entity_Id;
-- Referenced entity
Ref_Scope : Entity_Id;
-- Scope where the reference occurs
Rtype : Character;
-- Indicates type of the reference, using code used in ALI file:
-- r = reference
-- m = modification
-- s = call
end record;
-- This type holds a subset of the frontend xref entry that is needed by
-- the SPARK backend.
---------------
-- Constants --
---------------
Name_Of_Heap_Variable : constant String := "__HEAP";
-- Name of special variable used in effects to denote reads and writes
-- through explicit dereference.
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. Also, it is only created if there is
-- an actual need for it, and remains Empty otherwise.
-----------------
-- Subprograms --
-----------------
procedure dspark;
-- Debug routine to dump internal SPARK cross-reference tables. This is a
-- raw format dump showing exactly what the tables contain.
end SPARK_Xrefs;
|
