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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
//! A library for parsing Whiley test files according to
//! [RFC#110](https://github.com/Whiley/RFCs/blob/master/text/0110-test-file-format.md)
//! which are used for testing the [Whiley
//! compiler](https://github.com/Whiley/WhileyCompiler). Each test
//! describes a sequence of modifications to one of more Whiley files,
//! along with the expected outcomes (e.g. errors, warnings, etc). An
//! example test file is the following:
//! ```text
//! whiley.verify = false
//! boogie.timeout = 1000
//! ================
//! >>> main.whiley
//! method main():
//! >>> other.whiley
//! import main
//! ---
//! E101 main.whiley 1,2
//! E302 main.whiley 2,2:3
//! ================
//! <<< other.whiley
//! >>> main.whiley 1:1
//! method main()
//! skip
//! ---
//! ```
//! This is a test involving two files: `main.whiley` and `other.whiley`.
//! The initial frame sets the contents of `main.whiley` to `method
//! main()` and the contents of `other.whiley` to `import main`.
//! Furthermore, compiling this frame is expected to produce two errors
//! (`E101` and `E302`). The second frame deletes file `other.whiley` and
//! updates the contents of `main.whiley`. Furthermore, compiling the
//! snapshot at this point is not expected to produce any errors.
//!
//! ```
//! use std::fs;
//! use whiley_test_file::WhileyTestFile;
//!
//! fn load(filename: &str) {
//! // Read the test file
//! let input = fs::read_to_string(filename).unwrap();
//! // Parse test file
//! let test_file = WhileyTestFile::new(&input).unwrap();
//! // ...
//! }
//! ```
// Hidden modules
use Parser;
use HashMap;
use result;
// ===============================================================
// Error
// ===============================================================
pub type Result<T> = Result;
// ===============================================================
// Test File
// ===============================================================
// ===============================================================
// Config
// ===============================================================
type Config<'a> = ;
// ===============================================================
// Frame
// ===============================================================
/// Represents a frame within a testfile. Each frame identifies a
/// number of _actions_ which operate on the state at that point,
/// along with zero or more expected _markers_ (e.g. error messages).
/// The set of actions includes _inserting_ and _removing_ lines on a
/// specific file. Actions are applied in the order of appearance,
/// though they are not expected to overlap.
// ===============================================================
// Action
// ===============================================================
/// Represents an atomic action which can be applied to a source file,
/// such as inserting or replacing lines within the file.
// ===============================================================
// Marker
// ===============================================================
/// Identifies an expected error at a location in a given source file.
// ===============================================================
// Coordinate
// ===============================================================
/// Identifies a specific range of characters within a file.
;
// ===============================================================
// Range
// ===============================================================
/// Represents an interval (e.g. of characters within a line).
;