@@ -30,44 +30,6 @@ code_function_callt make_void_call(const symbol_exprt &function)
30
30
ret.function () = function;
31
31
return ret;
32
32
}
33
-
34
- void validate (
35
- const goto_functionst &goto_functions,
36
- const validation_modet vm,
37
- const goto_model_validation_optionst &goto_model_validation_options)
38
- {
39
- validate_goto_model (goto_functions, vm, goto_model_validation_options);
40
- }
41
-
42
- bool test_for_pass (
43
- goto_modelt &goto_model,
44
- const goto_model_validation_optionst goto_model_validation_options)
45
- {
46
- validate (
47
- goto_model.goto_functions ,
48
- validation_modet::INVARIANT,
49
- goto_model_validation_options);
50
- return true ;
51
- }
52
-
53
- bool test_for_failure (
54
- goto_modelt &goto_model,
55
- const goto_model_validation_optionst goto_model_validation_options)
56
- {
57
- bool caught{false };
58
- try
59
- {
60
- validate (
61
- goto_model.goto_functions ,
62
- validation_modet::EXCEPTION,
63
- goto_model_validation_options);
64
- }
65
- catch (incorrect_goto_program_exceptiont &e)
66
- {
67
- caught = true ;
68
- }
69
- return caught;
70
- }
71
33
} // namespace
72
34
73
35
SCENARIO (" validate goto program" )
@@ -153,10 +115,13 @@ SCENARIO("validate goto program")
153
115
154
116
THEN (" fail!" )
155
117
{
156
- goto_model_validation_optionst validation_options;
157
- validation_options.disable_all_checks ();
158
118
validation_options.entry_point_exists = true ;
159
- REQUIRE (test_for_failure (goto_model, validation_options));
119
+ REQUIRE_THROWS_AS (
120
+ validate_goto_model (
121
+ goto_model.goto_functions ,
122
+ validation_modet::EXCEPTION,
123
+ validation_options),
124
+ incorrect_goto_program_exceptiont);
160
125
}
161
126
}
162
127
@@ -165,10 +130,11 @@ SCENARIO("validate goto program")
165
130
goto_convert (goto_model, null_message_handler);
166
131
THEN (" pass!" )
167
132
{
168
- goto_model_validation_optionst validation_options;
169
- validation_options.disable_all_checks ();
170
133
validation_options.entry_point_exists = true ;
171
- REQUIRE (test_for_pass (goto_model, validation_options));
134
+ REQUIRE_NOTHROW (validate_goto_model (
135
+ goto_model.goto_functions ,
136
+ validation_modet::EXCEPTION,
137
+ validation_options));
172
138
}
173
139
}
174
140
@@ -195,10 +161,13 @@ SCENARIO("validate goto program")
195
161
196
162
goto_convert (goto_model, null_message_handler);
197
163
198
- goto_model_validation_optionst validation_options;
199
- validation_options.disable_all_checks ();
200
164
validation_options.function_pointer_calls_removed = true ;
201
- REQUIRE (test_for_failure (goto_model, validation_options));
165
+ REQUIRE_THROWS_AS (
166
+ validate_goto_model (
167
+ goto_model.goto_functions ,
168
+ validation_modet::EXCEPTION,
169
+ validation_options),
170
+ incorrect_goto_program_exceptiont);
202
171
}
203
172
}
204
173
@@ -208,10 +177,11 @@ SCENARIO("validate goto program")
208
177
{
209
178
goto_convert (goto_model, null_message_handler);
210
179
211
- goto_model_validation_optionst validation_options;
212
- validation_options.disable_all_checks ();
213
180
validation_options.function_pointer_calls_removed = true ;
214
- REQUIRE (test_for_pass (goto_model, validation_options));
181
+ REQUIRE_NOTHROW (validate_goto_model (
182
+ goto_model.goto_functions ,
183
+ validation_modet::EXCEPTION,
184
+ validation_options));
215
185
}
216
186
}
217
187
@@ -228,10 +198,13 @@ SCENARIO("validate goto program")
228
198
auto it = function_map.find (" f" );
229
199
it->second .type .return_type () = signedbv_typet{32 };
230
200
231
- goto_model_validation_optionst validation_options;
232
- validation_options.disable_all_checks ();
233
201
validation_options.check_returns_removed = true ;
234
- REQUIRE (test_for_failure (goto_model, validation_options));
202
+ REQUIRE_THROWS_AS (
203
+ validate_goto_model (
204
+ goto_model.goto_functions ,
205
+ validation_modet::EXCEPTION,
206
+ validation_options),
207
+ incorrect_goto_program_exceptiont);
235
208
}
236
209
}
237
210
@@ -252,10 +225,13 @@ SCENARIO("validate goto program")
252
225
auto &instructions = it->second .body .instructions ;
253
226
instructions.insert (instructions.begin (), instruction);
254
227
255
- goto_model_validation_optionst validation_options;
256
- validation_options.disable_all_checks ();
257
228
validation_options.check_returns_removed = true ;
258
- REQUIRE (test_for_failure (goto_model, validation_options));
229
+ REQUIRE_THROWS_AS (
230
+ validate_goto_model (
231
+ goto_model.goto_functions ,
232
+ validation_modet::EXCEPTION,
233
+ validation_options),
234
+ incorrect_goto_program_exceptiont);
259
235
}
260
236
}
261
237
@@ -287,10 +263,13 @@ SCENARIO("validate goto program")
287
263
{
288
264
goto_convert (goto_model, null_message_handler);
289
265
290
- goto_model_validation_optionst validation_options;
291
- validation_options.disable_all_checks ();
292
266
validation_options.check_returns_removed = true ;
293
- REQUIRE (test_for_failure (goto_model, validation_options));
267
+ REQUIRE_THROWS_AS (
268
+ validate_goto_model (
269
+ goto_model.goto_functions ,
270
+ validation_modet::EXCEPTION,
271
+ validation_options),
272
+ incorrect_goto_program_exceptiont);
294
273
}
295
274
}
296
275
@@ -300,10 +279,11 @@ SCENARIO("validate goto program")
300
279
{
301
280
goto_convert (goto_model, null_message_handler);
302
281
303
- goto_model_validation_optionst validation_options;
304
- validation_options.disable_all_checks ();
305
282
validation_options.check_returns_removed = true ;
306
- REQUIRE (test_for_pass (goto_model, validation_options));
283
+ REQUIRE_NOTHROW (validate_goto_model (
284
+ goto_model.goto_functions ,
285
+ validation_modet::EXCEPTION,
286
+ validation_options));
307
287
}
308
288
}
309
289
@@ -319,10 +299,13 @@ SCENARIO("validate goto program")
319
299
auto it = function_map.find (" g" );
320
300
function_map.erase (it);
321
301
322
- goto_model_validation_optionst validation_options;
323
- validation_options.disable_all_checks ();
324
302
validation_options.check_called_functions = true ;
325
- REQUIRE (test_for_failure (goto_model, validation_options));
303
+ REQUIRE_THROWS_AS (
304
+ validate_goto_model (
305
+ goto_model.goto_functions ,
306
+ validation_modet::EXCEPTION,
307
+ validation_options),
308
+ incorrect_goto_program_exceptiont);
326
309
}
327
310
}
328
311
@@ -336,10 +319,13 @@ SCENARIO("validate goto program")
336
319
auto it = function_map.find (" f" );
337
320
function_map.erase (it); // f is no longer in function map
338
321
339
- goto_model_validation_optionst validation_options;
340
- validation_options.disable_all_checks ();
341
322
validation_options.check_called_functions = true ;
342
- REQUIRE (test_for_failure (goto_model, validation_options));
323
+ REQUIRE_THROWS_AS (
324
+ validate_goto_model (
325
+ goto_model.goto_functions ,
326
+ validation_modet::EXCEPTION,
327
+ validation_options),
328
+ incorrect_goto_program_exceptiont);
343
329
}
344
330
}
345
331
@@ -351,10 +337,11 @@ SCENARIO("validate goto program")
351
337
{
352
338
goto_convert (goto_model, null_message_handler);
353
339
354
- goto_model_validation_optionst validation_options;
355
- validation_options.disable_all_checks ();
356
340
validation_options.check_called_functions = true ;
357
- REQUIRE (test_for_pass (goto_model, validation_options));
341
+ REQUIRE_NOTHROW (validate_goto_model (
342
+ goto_model.goto_functions ,
343
+ validation_modet::EXCEPTION,
344
+ validation_options));
358
345
}
359
346
}
360
347
@@ -369,10 +356,13 @@ SCENARIO("validate goto program")
369
356
it->second .body .instructions .erase (
370
357
std::prev (it->second .body .instructions .end ()));
371
358
372
- goto_model_validation_optionst validation_options;
373
- validation_options.disable_all_checks ();
374
359
validation_options.check_last_instruction = true ;
375
- REQUIRE (test_for_failure (goto_model, validation_options));
360
+ REQUIRE_THROWS_AS (
361
+ validate_goto_model (
362
+ goto_model.goto_functions ,
363
+ validation_modet::EXCEPTION,
364
+ validation_options),
365
+ incorrect_goto_program_exceptiont);
376
366
}
377
367
}
378
368
@@ -382,10 +372,11 @@ SCENARIO("validate goto program")
382
372
{
383
373
goto_convert (goto_model, null_message_handler);
384
374
385
- goto_model_validation_optionst validation_options;
386
- validation_options.disable_all_checks ();
387
375
validation_options.check_last_instruction = true ;
388
- REQUIRE (test_for_pass (goto_model, validation_options));
376
+ REQUIRE_NOTHROW (validate_goto_model (
377
+ goto_model.goto_functions ,
378
+ validation_modet::EXCEPTION,
379
+ validation_options));
389
380
}
390
381
}
391
382
@@ -401,10 +392,13 @@ SCENARIO("validate goto program")
401
392
it->second .body .instructions .front ().code .source_location ();
402
393
source_location.make_nil ();
403
394
404
- goto_model_validation_optionst validation_options;
405
- validation_options.disable_all_checks ();
406
395
validation_options.check_sourcecode_location = true ;
407
- REQUIRE (test_for_failure (goto_model, validation_options));
396
+ REQUIRE_THROWS_AS (
397
+ validate_goto_model (
398
+ goto_model.goto_functions ,
399
+ validation_modet::EXCEPTION,
400
+ validation_options),
401
+ incorrect_goto_program_exceptiont);
408
402
}
409
403
}
410
404
@@ -420,10 +414,13 @@ SCENARIO("validate goto program")
420
414
it->second .body .instructions .front ().source_location ;
421
415
source_location.make_nil ();
422
416
423
- goto_model_validation_optionst validation_options;
424
- validation_options.disable_all_checks ();
425
417
validation_options.check_sourcecode_location = true ;
426
- REQUIRE (test_for_failure (goto_model, validation_options));
418
+ REQUIRE_THROWS_AS (
419
+ validate_goto_model (
420
+ goto_model.goto_functions ,
421
+ validation_modet::EXCEPTION,
422
+ validation_options),
423
+ incorrect_goto_program_exceptiont);
427
424
}
428
425
}
429
426
}
0 commit comments