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