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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT 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 the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
---------------------------------------------------------------------------------------
-- --
-- Useful debug routines. They all "derive null ..." to minimize impact on --
-- self-analysis. --
-- --
--------------------------------------------------------------------------------
with Cells;
with CStacks;
with Dictionary;
with Heap;
with LexTokenManager;
with SeqAlgebra;
with STree;
use type Dictionary.Visibility;
--# inherit Cells,
--# CStacks,
--# Dictionary,
--# E_Strings,
--# Heap,
--# LexTokenManager,
--# SeqAlgebra,
--# SPARK_IO,
--# STree;
package Debug is
procedure PrintMsg (Msg : in String;
NewLine : in Boolean);
--# derives null from Msg,
--# NewLine;
-- Prints Sym to Standard_Output
procedure Print_Sym_Raw (Sym : in Dictionary.Symbol);
--# derives null from Sym;
-- Prints Msg, Sym, and a New_Line to Standard_Output
procedure Print_Sym (Msg : in String;
Sym : in Dictionary.Symbol);
--# derives null from Msg,
--# Sym;
-- Like Print_Sym, but produces more information (such as if the
-- function is a proof or ada function)
procedure Print_Function_Sym (Msg : in String;
Sym : in Dictionary.Symbol);
--# derives null from Msg,
--# Sym;
procedure PrintScope (Msg : in String;
Scope : in Dictionary.Scopes);
--# derives null from Msg,
--# Scope;
procedure PrintInt (Msg : in String;
I : in Integer);
--# derives null from I,
--# Msg;
procedure PrintBool (Msg : in String;
B : in Boolean);
--# derives null from B,
--# Msg;
procedure Print_Lex_Str (Msg : in String;
L : in LexTokenManager.Lex_String);
--# derives null from L,
--# Msg;
-- The_Heap needs to be "in out" here for DAG_IO.PrintDAG...
procedure PrintDAG
(Msg : in String;
DAG : in Cells.Cell;
The_Heap : in out Cells.Heap_Record;
Scope : in Dictionary.Scopes);
--# derives The_Heap from * &
--# null from DAG,
--# Msg,
--# Scope;
procedure Write_DAG_To_File
(Filename : in String;
DAG : in Cells.Cell;
The_Heap : in out Cells.Heap_Record;
Scope : in Dictionary.Scopes);
--# derives The_Heap from * &
--# null from DAG,
--# Filename,
--# Scope;
procedure Write_Heap_To_File (Filename : in String;
The_Heap : in out Cells.Heap_Record);
--# derives The_Heap from * &
--# null from Filename;
procedure Print_Cell (Msg : in String;
The_Heap : in out Cells.Heap_Record;
The_Cell : in Cells.Cell);
--# derives The_Heap from * &
--# null from Msg,
--# The_Cell;
procedure Print_Sym_Seq (Msg : in String;
Seq : in SeqAlgebra.Seq;
The_Heap : in Heap.HeapRecord);
--# derives null from Msg,
--# Seq,
--# The_Heap;
procedure PrintSeq (Msg : in String;
Seq : in SeqAlgebra.Seq;
The_Heap : in Heap.HeapRecord);
--# derives null from Msg,
--# Seq,
--# The_Heap;
procedure PrintNode (Msg : in String;
N : in STree.SyntaxNode);
--# derives null from Msg,
--# N;
procedure PrintTraceback (Msg : in String;
Depth : in Natural);
--# derives null from Depth,
--# Msg;
procedure Dump_Stack
(Msg : in String;
Scope : in Dictionary.Scopes;
VCG_Heap : in out Cells.Heap_Record;
Stack : in CStacks.Stack);
--# derives VCG_Heap from * &
--# null from Msg,
--# Scope,
--# Stack;
end Debug;
|
