Skip to content

Commit 3245e75

Browse files
romainbrenguierromainbrenguier
committed
Replace log.get_message_handler() calls
The calls will always return a reference to the field ui_message_handler which can be accessed directly instead.
1 parent 5c21913 commit 3245e75

File tree

8 files changed

+73
-74
lines changed

8 files changed

+73
-74
lines changed

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -372,7 +372,7 @@ int janalyzer_parse_optionst::doit()
372372
}
373373

374374
goto_model =
375-
initialize_goto_model(cmdline.args, log.get_message_handler(), options);
375+
initialize_goto_model(cmdline.args, ui_message_handler, options);
376376

377377
if(process_goto_program(options))
378378
return CPROVER_EXIT_INTERNAL_ERROR;
@@ -391,7 +391,7 @@ int janalyzer_parse_optionst::doit()
391391
{
392392
show_goto_functions(
393393
goto_model,
394-
log.get_message_handler(),
394+
ui_message_handler,
395395
ui_message_handler.get_ui(),
396396
cmdline.isset("list-goto-functions"));
397397
return CPROVER_EXIT_SUCCESS;
@@ -410,14 +410,14 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
410410
if(cmdline.isset("show-taint"))
411411
{
412412
taint_analysis(
413-
goto_model, taint_file, log.get_message_handler(), true, "");
413+
goto_model, taint_file, ui_message_handler, true, "");
414414
return CPROVER_EXIT_SUCCESS;
415415
}
416416
else
417417
{
418418
std::string json_file = cmdline.get_value("json");
419419
bool result = taint_analysis(
420-
goto_model, taint_file, log.get_message_handler(), false, json_file);
420+
goto_model, taint_file, ui_message_handler, false, json_file);
421421
return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
422422
}
423423
}
@@ -523,7 +523,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
523523
if(cmdline.isset("show-properties"))
524524
{
525525
show_properties(
526-
goto_model, log.get_message_handler(), ui_message_handler.get_ui());
526+
goto_model, ui_message_handler, ui_message_handler.get_ui());
527527
return CPROVER_EXIT_SUCCESS;
528528
}
529529

@@ -574,12 +574,12 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
574574
else if(options.get_bool_option("verify"))
575575
{
576576
result = static_verifier(
577-
goto_model, *analyzer, options, log.get_message_handler(), out);
577+
goto_model, *analyzer, options, ui_message_handler, out);
578578
}
579579
else if(options.get_bool_option("simplify"))
580580
{
581581
result = static_simplifier(
582-
goto_model, *analyzer, options, log.get_message_handler(), out);
582+
goto_model, *analyzer, options, ui_message_handler, out);
583583
}
584584
else if(options.get_bool_option("unreachable-instructions"))
585585
{
@@ -620,18 +620,18 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
620620
log.status() << "Removing function pointers and virtual functions"
621621
<< messaget::eom;
622622
remove_function_pointers(
623-
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
623+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
624624

625625
// Java virtual functions -> explicit dispatch tables:
626626
remove_virtual_functions(goto_model);
627627

628628
// remove Java throw and catch
629629
// This introduces instanceof, so order is important:
630-
remove_exceptions_using_instanceof(goto_model, log.get_message_handler());
630+
remove_exceptions_using_instanceof(goto_model, ui_message_handler);
631631

632632
// Java instanceof -> clsid comparison:
633633
class_hierarchyt class_hierarchy(goto_model.symbol_table);
634-
remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
634+
remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
635635

636636
// do partial inlining
637637
log.status() << "Partial Inlining" << messaget::eom;

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
138138
exit(CPROVER_EXIT_SUCCESS);
139139
}
140140

141-
parse_path_strategy_options(cmdline, options, log.get_message_handler());
141+
parse_path_strategy_options(cmdline, options, ui_message_handler);
142142

143143
if(cmdline.isset("program-only"))
144144
options.set_option("program-only", true);
@@ -427,7 +427,7 @@ int jbmc_parse_optionst::doit()
427427
messaget::eval_verbosity(
428428
cmdline.get_value("verbosity"),
429429
messaget::M_STATISTICS,
430-
log.get_message_handler());
430+
ui_message_handler);
431431

432432
//
433433
// command line options
@@ -502,7 +502,7 @@ int jbmc_parse_optionst::doit()
502502
}
503503

504504
language->set_language_options(options);
505-
language->set_message_handler(log.get_message_handler());
505+
language->set_message_handler(ui_message_handler);
506506

507507
log.status() << "Parsing " << filename << messaget::eom;
508508

@@ -566,7 +566,7 @@ int jbmc_parse_optionst::doit()
566566
if(cmdline.isset("show-properties"))
567567
{
568568
show_properties(
569-
goto_model, log.get_message_handler(), ui_message_handler.get_ui());
569+
goto_model, ui_message_handler, ui_message_handler.get_ui());
570570
return 0; // should contemplate EX_OK from sysexits.h
571571
}
572572

@@ -801,7 +801,7 @@ int jbmc_parse_optionst::get_goto_program(
801801
{
802802
show_goto_functions(
803803
*goto_model,
804-
log.get_message_handler(),
804+
ui_message_handler,
805805
ui_message_handler.get_ui(),
806806
cmdline.isset("list-goto-functions"));
807807
return 0;
@@ -832,7 +832,7 @@ void jbmc_parse_optionst::process_goto_function(
832832
goto_function,
833833
symbol_table,
834834
*class_hierarchy,
835-
log.get_message_handler());
835+
ui_message_handler);
836836
// Java virtual functions -> explicit dispatch tables:
837837
remove_virtual_functions(function);
838838

@@ -943,7 +943,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
943943
namespacet ns(goto_model.get_symbol_table());
944944
show_properties(
945945
ns,
946-
log.get_message_handler(),
946+
ui_message_handler,
947947
ui_message_handler.get_ui(),
948948
goto_model.get_goto_functions());
949949
return true;
@@ -970,7 +970,7 @@ bool jbmc_parse_optionst::process_goto_functions(
970970

971971
// remove catch and throw
972972
remove_exceptions(
973-
goto_model, *class_hierarchy.get(), log.get_message_handler());
973+
goto_model, *class_hierarchy.get(), ui_message_handler);
974974

975975
// instrument library preconditions
976976
instrument_preconditions(goto_model);
@@ -992,7 +992,7 @@ bool jbmc_parse_optionst::process_goto_functions(
992992
{
993993
// Entry point will have been set before and function pointers removed
994994
log.status() << "Removing unused functions" << messaget::eom;
995-
remove_unused_functions(goto_model, log.get_message_handler());
995+
remove_unused_functions(goto_model, ui_message_handler);
996996
}
997997

998998
// remove skips such that trivial GOTOs are deleted

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -228,12 +228,12 @@ int jdiff_parse_optionst::doit()
228228
{
229229
show_goto_functions(
230230
goto_model1,
231-
log.get_message_handler(),
231+
ui_message_handler,
232232
ui_message_handler.get_ui(),
233233
cmdline.isset("list-goto-functions"));
234234
show_goto_functions(
235235
goto_model2,
236-
log.get_message_handler(),
236+
ui_message_handler,
237237
ui_message_handler.get_ui(),
238238
cmdline.isset("list-goto-functions"));
239239
return CPROVER_EXIT_SUCCESS;
@@ -279,18 +279,18 @@ bool jdiff_parse_optionst::process_goto_program(
279279
log.status() << "Removing function pointers and virtual functions"
280280
<< messaget::eom;
281281
remove_function_pointers(
282-
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
282+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
283283

284284
// Java virtual functions -> explicit dispatch tables:
285285
remove_virtual_functions(goto_model);
286286

287287
// remove Java throw and catch
288288
// This introduces instanceof, so order is important:
289-
remove_exceptions_using_instanceof(goto_model, log.get_message_handler());
289+
remove_exceptions_using_instanceof(goto_model, ui_message_handler);
290290

291291
// Java instanceof -> clsid comparison:
292292
class_hierarchyt class_hierarchy(goto_model.symbol_table);
293-
remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
293+
remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
294294

295295
mm_io(goto_model);
296296

@@ -324,9 +324,9 @@ bool jdiff_parse_optionst::process_goto_program(
324324
if(cmdline.isset("cover"))
325325
{
326326
const auto cover_config = get_cover_config(
327-
options, goto_model.symbol_table, log.get_message_handler());
327+
options, goto_model.symbol_table, ui_message_handler);
328328
if(instrument_cover_goals(
329-
cover_config, goto_model, log.get_message_handler()))
329+
cover_config, goto_model, ui_message_handler))
330330
return true;
331331
}
332332

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -486,7 +486,7 @@ int cbmc_parse_optionst::doit()
486486
register_languages();
487487

488488
if(cmdline.isset("test-preprocessor"))
489-
return test_c_preprocessor(log.get_message_handler())
489+
return test_c_preprocessor(ui_message_handler)
490490
? CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
491491
: CPROVER_EXIT_SUCCESS;
492492

@@ -532,7 +532,7 @@ int cbmc_parse_optionst::doit()
532532
}
533533

534534
language->set_language_options(options);
535-
language->set_message_handler(log.get_message_handler());
535+
language->set_message_handler(ui_message_handler);
536536

537537
log.status() << "Parsing " << filename << messaget::eom;
538538

@@ -556,7 +556,7 @@ int cbmc_parse_optionst::doit()
556556
cmdline.isset("show-properties")) // use this one
557557
{
558558
show_properties(
559-
goto_model, log.get_message_handler(), ui_message_handler.get_ui());
559+
goto_model, ui_message_handler, ui_message_handler.get_ui());
560560
return CPROVER_EXIT_SUCCESS;
561561
}
562562

@@ -774,7 +774,7 @@ void cbmc_parse_optionst::preprocessing(const optionst &options)
774774
return;
775775
}
776776

777-
language->set_message_handler(log.get_message_handler());
777+
language->set_message_handler(ui_message_handler);
778778

779779
if(language->preprocess(infile, filename, std::cout))
780780
log.error() << "PREPROCESSING ERROR" << messaget::eom;

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -401,8 +401,7 @@ int goto_analyzer_parse_optionst::doit()
401401

402402
register_languages();
403403

404-
goto_model =
405-
initialize_goto_model(cmdline.args, log.get_message_handler(), options);
404+
goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
406405

407406
if(process_goto_program(options))
408407
return CPROVER_EXIT_INTERNAL_ERROR;
@@ -426,7 +425,7 @@ int goto_analyzer_parse_optionst::doit()
426425
{
427426
show_goto_functions(
428427
goto_model,
429-
log.get_message_handler(),
428+
ui_message_handler,
430429
ui_message_handler.get_ui(),
431430
cmdline.isset("list-goto-functions"));
432431
return CPROVER_EXIT_SUCCESS;
@@ -447,14 +446,14 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
447446
if(cmdline.isset("show-taint"))
448447
{
449448
taint_analysis(
450-
goto_model, taint_file, log.get_message_handler(), true, "");
449+
goto_model, taint_file, ui_message_handler, true, "");
451450
return CPROVER_EXIT_SUCCESS;
452451
}
453452
else
454453
{
455454
std::string json_file=cmdline.get_value("json");
456455
bool result = taint_analysis(
457-
goto_model, taint_file, log.get_message_handler(), false, json_file);
456+
goto_model, taint_file, ui_message_handler, false, json_file);
458457
return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
459458
}
460459
}
@@ -558,7 +557,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
558557
{
559558
show_properties(
560559
goto_model,
561-
log.get_message_handler(),
560+
ui_message_handler,
562561
ui_message_handler.get_ui());
563562
return CPROVER_EXIT_SUCCESS;
564563
}
@@ -613,21 +612,21 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
613612
}
614613
else if(options.get_bool_option("show-on-source"))
615614
{
616-
show_on_source(goto_model, *analyzer, log.get_message_handler());
615+
show_on_source(goto_model, *analyzer, ui_message_handler);
617616
return CPROVER_EXIT_SUCCESS;
618617
}
619618
else if(options.get_bool_option("verify"))
620619
{
621620
result = static_verifier(
622-
goto_model, *analyzer, options, log.get_message_handler(), out);
621+
goto_model, *analyzer, options, ui_message_handler, out);
623622
}
624623
else if(options.get_bool_option("simplify"))
625624
{
626625
PRECONDITION(!outfile.empty() && outfile != "-");
627626
output_stream.close();
628627
output_stream.open(outfile, std::ios::binary);
629628
result = static_simplifier(
630-
goto_model, *analyzer, options, log.get_message_handler(), out);
629+
goto_model, *analyzer, options, ui_message_handler, out);
631630
}
632631
else if(options.get_bool_option("unreachable-instructions"))
633632
{
@@ -687,7 +686,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
687686
log.status() << "Removing function pointers and virtual functions"
688687
<< messaget::eom;
689688
remove_function_pointers(
690-
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
689+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
691690

692691
// do partial inlining
693692
log.status() << "Partial Inlining" << messaget::eom;

‎src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -266,12 +266,12 @@ int goto_diff_parse_optionst::doit()
266266
{
267267
show_goto_functions(
268268
goto_model1,
269-
log.get_message_handler(),
269+
ui_message_handler,
270270
ui_message_handler.get_ui(),
271271
cmdline.isset("list-goto-functions"));
272272
show_goto_functions(
273273
goto_model2,
274-
log.get_message_handler(),
274+
ui_message_handler,
275275
ui_message_handler.get_ui(),
276276
cmdline.isset("list-goto-functions"));
277277
return CPROVER_EXIT_SUCCESS;
@@ -326,15 +326,15 @@ bool goto_diff_parse_optionst::process_goto_program(
326326
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
327327
<< messaget::eom;
328328
link_to_library(
329-
goto_model, log.get_message_handler(), cprover_cpp_library_factory);
329+
goto_model, ui_message_handler, cprover_cpp_library_factory);
330330
link_to_library(
331-
goto_model, log.get_message_handler(), cprover_c_library_factory);
331+
goto_model, ui_message_handler, cprover_c_library_factory);
332332

333333
// remove function pointers
334334
log.status() << "Removal of function pointers and virtual functions"
335335
<< messaget::eom;
336336
remove_function_pointers(
337-
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
337+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
338338

339339
mm_io(goto_model);
340340

@@ -368,9 +368,9 @@ bool goto_diff_parse_optionst::process_goto_program(
368368
remove_skip(goto_model);
369369

370370
const auto cover_config = get_cover_config(
371-
options, goto_model.symbol_table, log.get_message_handler());
371+
options, goto_model.symbol_table, ui_message_handler);
372372
if(instrument_cover_goals(
373-
cover_config, goto_model, log.get_message_handler()))
373+
cover_config, goto_model, ui_message_handler))
374374
return true;
375375
}
376376

‎src/goto-harness/goto_harness_parse_options.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ int goto_harness_parse_optionst::doit()
5555

5656
// Read goto binary into goto-model
5757
auto read_goto_binary_result =
58-
read_goto_binary(got_harness_config.in_file, log.get_message_handler());
58+
read_goto_binary(got_harness_config.in_file, ui_message_handler);
5959
if(!read_goto_binary_result.has_value())
6060
{
6161
throw deserialization_exceptiont{"failed to read goto program from file `" +
@@ -89,7 +89,7 @@ int goto_harness_parse_optionst::doit()
8989

9090
// Write end result to new goto-binary
9191
if(write_goto_binary(
92-
got_harness_config.out_file, goto_model, log.get_message_handler()))
92+
got_harness_config.out_file, goto_model, ui_message_handler))
9393
{
9494
throw system_exceptiont{"failed to write goto program from file `" +
9595
got_harness_config.out_file + "'"};

0 commit comments

Comments
 (0)