Skip to content

Commit 79b4117

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 57be244 commit 79b4117

8 files changed

+51
-62
lines changed

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -371,8 +371,7 @@ int janalyzer_parse_optionst::doit()
371371
return CPROVER_EXIT_USAGE_ERROR;
372372
}
373373

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

377376
if(process_goto_program(options))
378377
return CPROVER_EXIT_INTERNAL_ERROR;
@@ -391,7 +390,7 @@ int janalyzer_parse_optionst::doit()
391390
{
392391
show_goto_functions(
393392
goto_model,
394-
log.get_message_handler(),
393+
ui_message_handler,
395394
ui_message_handler.get_ui(),
396395
cmdline.isset("list-goto-functions"));
397396
return CPROVER_EXIT_SUCCESS;
@@ -409,15 +408,14 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
409408

410409
if(cmdline.isset("show-taint"))
411410
{
412-
taint_analysis(
413-
goto_model, taint_file, log.get_message_handler(), true, "");
411+
taint_analysis(goto_model, taint_file, ui_message_handler, true, "");
414412
return CPROVER_EXIT_SUCCESS;
415413
}
416414
else
417415
{
418416
std::string json_file = cmdline.get_value("json");
419417
bool result = taint_analysis(
420-
goto_model, taint_file, log.get_message_handler(), false, json_file);
418+
goto_model, taint_file, ui_message_handler, false, json_file);
421419
return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
422420
}
423421
}
@@ -523,7 +521,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
523521
if(cmdline.isset("show-properties"))
524522
{
525523
show_properties(
526-
goto_model, log.get_message_handler(), ui_message_handler.get_ui());
524+
goto_model, ui_message_handler, ui_message_handler.get_ui());
527525
return CPROVER_EXIT_SUCCESS;
528526
}
529527

@@ -574,12 +572,12 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
574572
else if(options.get_bool_option("verify"))
575573
{
576574
result = static_verifier(
577-
goto_model, *analyzer, options, log.get_message_handler(), out);
575+
goto_model, *analyzer, options, ui_message_handler, out);
578576
}
579577
else if(options.get_bool_option("simplify"))
580578
{
581579
result = static_simplifier(
582-
goto_model, *analyzer, options, log.get_message_handler(), out);
580+
goto_model, *analyzer, options, ui_message_handler, out);
583581
}
584582
else if(options.get_bool_option("unreachable-instructions"))
585583
{
@@ -620,18 +618,18 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
620618
log.status() << "Removing function pointers and virtual functions"
621619
<< messaget::eom;
622620
remove_function_pointers(
623-
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
621+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
624622

625623
// Java virtual functions -> explicit dispatch tables:
626624
remove_virtual_functions(goto_model);
627625

628626
// remove Java throw and catch
629627
// This introduces instanceof, so order is important:
630-
remove_exceptions_using_instanceof(goto_model, log.get_message_handler());
628+
remove_exceptions_using_instanceof(goto_model, ui_message_handler);
631629

632630
// Java instanceof -> clsid comparison:
633631
class_hierarchyt class_hierarchy(goto_model.symbol_table);
634-
remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
632+
remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
635633

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

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 9 additions & 12 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);
@@ -425,9 +425,7 @@ int jbmc_parse_optionst::doit()
425425
}
426426

427427
messaget::eval_verbosity(
428-
cmdline.get_value("verbosity"),
429-
messaget::M_STATISTICS,
430-
log.get_message_handler());
428+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
431429

432430
//
433431
// command line options
@@ -502,7 +500,7 @@ int jbmc_parse_optionst::doit()
502500
}
503501

504502
language->set_language_options(options);
505-
language->set_message_handler(log.get_message_handler());
503+
language->set_message_handler(ui_message_handler);
506504

507505
log.status() << "Parsing " << filename << messaget::eom;
508506

@@ -566,7 +564,7 @@ int jbmc_parse_optionst::doit()
566564
if(cmdline.isset("show-properties"))
567565
{
568566
show_properties(
569-
goto_model, log.get_message_handler(), ui_message_handler.get_ui());
567+
goto_model, ui_message_handler, ui_message_handler.get_ui());
570568
return 0; // should contemplate EX_OK from sysexits.h
571569
}
572570

@@ -801,7 +799,7 @@ int jbmc_parse_optionst::get_goto_program(
801799
{
802800
show_goto_functions(
803801
*goto_model,
804-
log.get_message_handler(),
802+
ui_message_handler,
805803
ui_message_handler.get_ui(),
806804
cmdline.isset("list-goto-functions"));
807805
return 0;
@@ -832,7 +830,7 @@ void jbmc_parse_optionst::process_goto_function(
832830
goto_function,
833831
symbol_table,
834832
*class_hierarchy,
835-
log.get_message_handler());
833+
ui_message_handler);
836834
// Java virtual functions -> explicit dispatch tables:
837835
remove_virtual_functions(function);
838836

@@ -944,7 +942,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
944942
namespacet ns(goto_model.get_symbol_table());
945943
show_properties(
946944
ns,
947-
log.get_message_handler(),
945+
ui_message_handler,
948946
ui_message_handler.get_ui(),
949947
goto_model.get_goto_functions());
950948
return true;
@@ -970,8 +968,7 @@ bool jbmc_parse_optionst::process_goto_functions(
970968
return false;
971969

972970
// remove catch and throw
973-
remove_exceptions(
974-
goto_model, *class_hierarchy.get(), log.get_message_handler());
971+
remove_exceptions(goto_model, *class_hierarchy.get(), ui_message_handler);
975972

976973
// instrument library preconditions
977974
instrument_preconditions(goto_model);
@@ -993,7 +990,7 @@ bool jbmc_parse_optionst::process_goto_functions(
993990
{
994991
// Entry point will have been set before and function pointers removed
995992
log.status() << "Removing unused functions" << messaget::eom;
996-
remove_unused_functions(goto_model, log.get_message_handler());
993+
remove_unused_functions(goto_model, ui_message_handler);
997994
}
998995

999996
// remove skips such that trivial GOTOs are deleted

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 8 additions & 9 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;
@@ -280,18 +280,18 @@ bool jdiff_parse_optionst::process_goto_program(
280280
log.status() << "Removing function pointers and virtual functions"
281281
<< messaget::eom;
282282
remove_function_pointers(
283-
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
283+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
284284

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

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

292292
// Java instanceof -> clsid comparison:
293293
class_hierarchyt class_hierarchy(goto_model.symbol_table);
294-
remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
294+
remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
295295

296296
mm_io(goto_model);
297297

@@ -324,10 +324,9 @@ bool jdiff_parse_optionst::process_goto_program(
324324
// instrument cover goals
325325
if(cmdline.isset("cover"))
326326
{
327-
const auto cover_config = get_cover_config(
328-
options, goto_model.symbol_table, log.get_message_handler());
329-
if(instrument_cover_goals(
330-
cover_config, goto_model, log.get_message_handler()))
327+
const auto cover_config =
328+
get_cover_config(options, goto_model.symbol_table, ui_message_handler);
329+
if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
331330
return true;
332331
}
333332

‎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 & 11 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;
@@ -446,15 +445,14 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
446445

447446
if(cmdline.isset("show-taint"))
448447
{
449-
taint_analysis(
450-
goto_model, taint_file, log.get_message_handler(), true, "");
448+
taint_analysis(goto_model, taint_file, ui_message_handler, true, "");
451449
return CPROVER_EXIT_SUCCESS;
452450
}
453451
else
454452
{
455453
std::string json_file=cmdline.get_value("json");
456454
bool result = taint_analysis(
457-
goto_model, taint_file, log.get_message_handler(), false, json_file);
455+
goto_model, taint_file, ui_message_handler, false, json_file);
458456
return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
459457
}
460458
}
@@ -557,7 +555,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
557555
if(cmdline.isset("show-properties"))
558556
{
559557
show_properties(
560-
goto_model, log.get_message_handler(), ui_message_handler.get_ui());
558+
goto_model, ui_message_handler, ui_message_handler.get_ui());
561559
return CPROVER_EXIT_SUCCESS;
562560
}
563561

@@ -611,21 +609,21 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
611609
}
612610
else if(options.get_bool_option("show-on-source"))
613611
{
614-
show_on_source(goto_model, *analyzer, log.get_message_handler());
612+
show_on_source(goto_model, *analyzer, ui_message_handler);
615613
return CPROVER_EXIT_SUCCESS;
616614
}
617615
else if(options.get_bool_option("verify"))
618616
{
619617
result = static_verifier(
620-
goto_model, *analyzer, options, log.get_message_handler(), out);
618+
goto_model, *analyzer, options, ui_message_handler, out);
621619
}
622620
else if(options.get_bool_option("simplify"))
623621
{
624622
PRECONDITION(!outfile.empty() && outfile != "-");
625623
output_stream.close();
626624
output_stream.open(outfile, std::ios::binary);
627625
result = static_simplifier(
628-
goto_model, *analyzer, options, log.get_message_handler(), out);
626+
goto_model, *analyzer, options, ui_message_handler, out);
629627
}
630628
else if(options.get_bool_option("unreachable-instructions"))
631629
{
@@ -685,7 +683,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
685683
log.status() << "Removing function pointers and virtual functions"
686684
<< messaget::eom;
687685
remove_function_pointers(
688-
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
686+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
689687

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

‎src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 8 additions & 10 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,14 @@ 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);
330-
link_to_library(
331-
goto_model, log.get_message_handler(), cprover_c_library_factory);
329+
goto_model, ui_message_handler, cprover_cpp_library_factory);
330+
link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
332331

333332
// remove function pointers
334333
log.status() << "Removal of function pointers and virtual functions"
335334
<< messaget::eom;
336335
remove_function_pointers(
337-
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
336+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
338337

339338
mm_io(goto_model);
340339

@@ -367,10 +366,9 @@ bool goto_diff_parse_optionst::process_goto_program(
367366
// for coverage annotation:
368367
remove_skip(goto_model);
369368

370-
const auto cover_config = get_cover_config(
371-
options, goto_model.symbol_table, log.get_message_handler());
372-
if(instrument_cover_goals(
373-
cover_config, goto_model, log.get_message_handler()))
369+
const auto cover_config =
370+
get_cover_config(options, goto_model.symbol_table, ui_message_handler);
371+
if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
374372
return true;
375373
}
376374

‎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)