@@ -115,6 +115,7 @@ SCENARIO("validate goto program")
115
115
116
116
THEN (" fail!" )
117
117
{
118
+ goto_model_validation_optionst validation_options{false };
118
119
validation_options.entry_point_exists = true ;
119
120
REQUIRE_THROWS_AS (
120
121
validate_goto_model (
@@ -130,6 +131,7 @@ SCENARIO("validate goto program")
130
131
goto_convert (goto_model, null_message_handler);
131
132
THEN (" pass!" )
132
133
{
134
+ goto_model_validation_optionst validation_options{false };
133
135
validation_options.entry_point_exists = true ;
134
136
REQUIRE_NOTHROW (validate_goto_model (
135
137
goto_model.goto_functions ,
@@ -161,6 +163,7 @@ SCENARIO("validate goto program")
161
163
162
164
goto_convert (goto_model, null_message_handler);
163
165
166
+ goto_model_validation_optionst validation_options{false };
164
167
validation_options.function_pointer_calls_removed = true ;
165
168
REQUIRE_THROWS_AS (
166
169
validate_goto_model (
@@ -177,6 +180,7 @@ SCENARIO("validate goto program")
177
180
{
178
181
goto_convert (goto_model, null_message_handler);
179
182
183
+ goto_model_validation_optionst validation_options{false };
180
184
validation_options.function_pointer_calls_removed = true ;
181
185
REQUIRE_NOTHROW (validate_goto_model (
182
186
goto_model.goto_functions ,
@@ -198,6 +202,7 @@ SCENARIO("validate goto program")
198
202
auto it = function_map.find (" f" );
199
203
it->second .type .return_type () = signedbv_typet{32 };
200
204
205
+ goto_model_validation_optionst validation_options{false };
201
206
validation_options.check_returns_removed = true ;
202
207
REQUIRE_THROWS_AS (
203
208
validate_goto_model (
@@ -225,6 +230,7 @@ SCENARIO("validate goto program")
225
230
auto &instructions = it->second .body .instructions ;
226
231
instructions.insert (instructions.begin (), instruction);
227
232
233
+ goto_model_validation_optionst validation_options{false };
228
234
validation_options.check_returns_removed = true ;
229
235
REQUIRE_THROWS_AS (
230
236
validate_goto_model (
@@ -263,6 +269,7 @@ SCENARIO("validate goto program")
263
269
{
264
270
goto_convert (goto_model, null_message_handler);
265
271
272
+ goto_model_validation_optionst validation_options{false };
266
273
validation_options.check_returns_removed = true ;
267
274
REQUIRE_THROWS_AS (
268
275
validate_goto_model (
@@ -279,6 +286,7 @@ SCENARIO("validate goto program")
279
286
{
280
287
goto_convert (goto_model, null_message_handler);
281
288
289
+ goto_model_validation_optionst validation_options{false };
282
290
validation_options.check_returns_removed = true ;
283
291
REQUIRE_NOTHROW (validate_goto_model (
284
292
goto_model.goto_functions ,
@@ -299,6 +307,7 @@ SCENARIO("validate goto program")
299
307
auto it = function_map.find (" g" );
300
308
function_map.erase (it);
301
309
310
+ goto_model_validation_optionst validation_options{false };
302
311
validation_options.check_called_functions = true ;
303
312
REQUIRE_THROWS_AS (
304
313
validate_goto_model (
@@ -319,6 +328,7 @@ SCENARIO("validate goto program")
319
328
auto it = function_map.find (" f" );
320
329
function_map.erase (it); // f is no longer in function map
321
330
331
+ goto_model_validation_optionst validation_options{false };
322
332
validation_options.check_called_functions = true ;
323
333
REQUIRE_THROWS_AS (
324
334
validate_goto_model (
@@ -337,6 +347,7 @@ SCENARIO("validate goto program")
337
347
{
338
348
goto_convert (goto_model, null_message_handler);
339
349
350
+ goto_model_validation_optionst validation_options{false };
340
351
validation_options.check_called_functions = true ;
341
352
REQUIRE_NOTHROW (validate_goto_model (
342
353
goto_model.goto_functions ,
@@ -356,6 +367,7 @@ SCENARIO("validate goto program")
356
367
it->second .body .instructions .erase (
357
368
std::prev (it->second .body .instructions .end ()));
358
369
370
+ goto_model_validation_optionst validation_options{false };
359
371
validation_options.check_last_instruction = true ;
360
372
REQUIRE_THROWS_AS (
361
373
validate_goto_model (
@@ -372,6 +384,7 @@ SCENARIO("validate goto program")
372
384
{
373
385
goto_convert (goto_model, null_message_handler);
374
386
387
+ goto_model_validation_optionst validation_options{false };
375
388
validation_options.check_last_instruction = true ;
376
389
REQUIRE_NOTHROW (validate_goto_model (
377
390
goto_model.goto_functions ,
@@ -392,6 +405,7 @@ SCENARIO("validate goto program")
392
405
it->second .body .instructions .front ().code .source_location ();
393
406
source_location.make_nil ();
394
407
408
+ goto_model_validation_optionst validation_options{false };
395
409
validation_options.check_sourcecode_location = true ;
396
410
REQUIRE_THROWS_AS (
397
411
validate_goto_model (
@@ -414,6 +428,7 @@ SCENARIO("validate goto program")
414
428
it->second .body .instructions .front ().source_location ;
415
429
source_location.make_nil ();
416
430
431
+ goto_model_validation_optionst validation_options{false };
417
432
validation_options.check_sourcecode_location = true ;
418
433
REQUIRE_THROWS_AS (
419
434
validate_goto_model (
0 commit comments