projects / thirdparty / gcc.git / blame
| Commit | Line | Data |
|---|---|---|
| 56e94186 AC |
1 | ------------------------------------------------------------------------------ |
| 2 | -- -- | |
| 3 | -- GNAT COMPILER COMPONENTS -- | |
| 4 | -- -- | |
| 06b599fd | 5 | -- S P A R K _ X R E F S -- |
| 56e94186 AC |
6 | -- -- |
| 7 | -- S p e c -- | |
| 8 | -- -- | |
| 1d005acc | 9 | -- Copyright (C) 2011-2019, Free Software Foundation, Inc. -- |
| 56e94186 AC |
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 | ||
| c23f55b4 PMR |
26 | -- This package defines data structures used to expose frontend |
| 27 | -- cross-references to the SPARK backend. | |
| 56e94186 | 28 | |
| 7cc7f3aa | 29 | with Types; use Types; |
| 56e94186 | 30 | |
| 06b599fd | 31 | package SPARK_Xrefs is |
| 56e94186 | 32 | |
| 06b599fd | 33 | type SPARK_Xref_Record is record |
| 3e5400f4 | 34 | Entity : Entity_Id; |
| 2cf8eabd | 35 | -- Referenced entity |
| 56e94186 | 36 | |
| 2cf8eabd PMR |
37 | Ref_Scope : Entity_Id; |
| 38 | -- Scope where the reference occurs | |
| 56e94186 | 39 | |
| 56e94186 | 40 | Rtype : Character; |
| 10c2c151 | 41 | -- Indicates type of the reference, using code used in ALI file: |
| 56e94186 AC |
42 | -- r = reference |
| 43 | -- m = modification | |
| 44 | -- s = call | |
| 56e94186 | 45 | end record; |
| c23f55b4 PMR |
46 | -- This type holds a subset of the frontend xref entry that is needed by |
| 47 | -- the SPARK backend. | |
| 56e94186 | 48 | |
| 226a7fa4 AC |
49 | --------------- |
| 50 | -- Constants -- | |
| 51 | --------------- | |
| 52 | ||
| 24a120ac | 53 | Name_Of_Heap_Variable : constant String := "__HEAP"; |
| 226a7fa4 AC |
54 | -- Name of special variable used in effects to denote reads and writes |
| 55 | -- through explicit dereference. | |
| 56 | ||
| 3e5400f4 PMR |
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 | ||
| 56e94186 AC |
62 | ----------------- |
| 63 | -- Subprograms -- | |
| 64 | ----------------- | |
| 65 | ||
| 06b599fd YM |
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. | |
| 824e9320 | 69 | |
| 06b599fd | 70 | end SPARK_Xrefs; |