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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
using System.IO;
using System.Collections;
using System.Collections.Generic;
using System.Text;
using Microsoft.Contracts;
using Bpl = Microsoft.Boogie;
using BoogiePL;
namespace Microsoft.Dafny {
[Immutable]
public class Token : Bpl.Token {
public Token();
public Token(int linenum, int colnum) {
base(linenum, colnum);
}
public new static Token! NoToken = new Token();
}
}
namespace Microsoft.-->namespace {
public class Scanner {
const char EOF = '\0';
const char CR = '\r';
const char LF = '\n';
[Microsoft.Contracts.Verify(false)]
-->declarations
static Token/*!*/ t; // current token
static char ch; // current input character
static int pos; // column number of current character
static int line; // line number of current character
static int lineStart; // start position of current line
static Queue! oldEols; // EOLs that appeared in a comment;
static BitArray/*!*/ ignore; // set of characters to be ignored by the scanner
static string Filename;
///<summary>
///Initializes the scanner. Note: first fill the Buffer.
///</summary>
///<param name="filename">File name used for error reporting</param>
public static void Init (string filename) {
Filename = filename;
pos = -1; line = 1; lineStart = 0;
oldEols = new Queue();
NextCh();
-->initialization
}
private static void NextCh() {
if (oldEols.Count > 0) {
ch = (char) ((!)oldEols.Dequeue());
} else {
while (true) {
ch = (char)BoogiePL.Buffer.Read(); pos++;
if (ch == BoogiePL.Buffer.eof) {
ch = EOF;
} else if (ch == LF) {
line++;
lineStart = pos + 1;
} else if (ch == '#' && pos == lineStart) {
int prLine = line;
int prColumn = pos - lineStart; // which is 0
string hashLine = BoogiePL.Buffer.ReadToEOL(); pos += hashLine.Length;
line++;
lineStart = pos + 1;
hashLine = hashLine.TrimEnd(null);
if (hashLine.StartsWith("line ") || hashLine == "line") {
// parse #line pragma: #line num [filename]
string h = hashLine.Substring(4).TrimStart(null);
int x = h.IndexOf(' ');
if (x == -1) {
x = h.Length; // this will be convenient below when we look for a filename
}
try {
int li = int.Parse(h.Substring(0, x));
h = h.Substring(x).Trim();
// act on #line
line = li;
if (h.Length != 0) {
// a filename was specified
Filename = h;
}
continue; // successfully parsed and acted on the #line pragma
} catch (System.FormatException) {
// just fall down through to produce an error message
}
Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);
continue;
}
Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);
continue;
}
return;
}
}
}
-->comment
static void CheckLiteral() {
switch (t.val) {
-->literals
}
}
public static Token/*!*/ Scan() {
while (ignore[ch]) { NextCh(); }
-->scan1
t = new Token();
t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;
int state = (/*^ (!) ^*/ start)[ch];
StringBuilder buf = new StringBuilder(16);
buf.Append(ch); NextCh();
switch (state) {
case 0: {t.kind = noSym; goto done;} // NextCh already done
-->scan2
}
done:
t.val = buf.ToString();
return t;
}
} // end Scanner
public delegate void ErrorProc(int n, string filename, int line, int col);
public class Errors {
public static int count = 0; // number of errors detected
public static ErrorProc/*!*/ SynErr; // syntactic errors
public static void SemErr(string filename, int line, int col, string! msg) { // semantic errors
System.ConsoleColor color = System.Console.ForegroundColor;
System.Console.ForegroundColor = System.ConsoleColor.Red;
System.Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);
System.Console.ForegroundColor = color;
count++;
}
public static void SemErr(Bpl.IToken! tok, string! msg) { // semantic errors
SemErr(tok.filename, tok.line, tok.col, msg);
}
public static void Exception (string s) {
System.ConsoleColor color = System.Console.ForegroundColor;
System.Console.ForegroundColor = System.ConsoleColor.Red;
System.Console.WriteLine(s);
System.Console.ForegroundColor = color;
System.Environment.Exit(0);
}
} // Errors
} // end namespace
$$$
|
