Skip to content

Commit 37873f3

Browse files
romainbrenguierromainbrenguier
committed
Make parse_options_baset the owner of message_handler
The message handler field was owned by the classes inheriting from parse_options_baset which lead to strange patterns where the handler reference was initialized using a reference to a field which was not constructed yet. This is cleaner and avoid some reference duplications.
1 parent c57a132 commit 37873f3

19 files changed

+135
-134
lines changed

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,11 @@ Author: Daniel Kroening, [email protected]
5858
#include <goto-analyzer/unreachable_instructions.h>
5959

6060
janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
61-
: parse_options_baset(JANALYZER_OPTIONS, argc, argv, ui_message_handler),
62-
ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
61+
: parse_options_baset(
62+
JANALYZER_OPTIONS,
63+
argc,
64+
argv,
65+
std::string("JANALYZER ") + CBMC_VERSION)
6366
{
6467
}
6568

@@ -344,7 +347,7 @@ int janalyzer_parse_optionst::doit()
344347
optionst options;
345348
get_command_line_options(options);
346349
messaget::eval_verbosity(
347-
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
350+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, *message_handler);
348351

349352
//
350353
// Print a banner
@@ -377,7 +380,7 @@ int janalyzer_parse_optionst::doit()
377380
// show it?
378381
if(cmdline.isset("show-symbol-table"))
379382
{
380-
::show_symbol_table(goto_model.symbol_table, ui_message_handler);
383+
::show_symbol_table(goto_model.symbol_table, *message_handler);
381384
return CPROVER_EXIT_SUCCESS;
382385
}
383386

@@ -631,7 +634,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
631634

632635
// do partial inlining
633636
log.status() << "Partial Inlining" << messaget::eom;
634-
goto_partial_inline(goto_model, ui_message_handler);
637+
goto_partial_inline(goto_model, *message_handler);
635638

636639
// remove returns, gcc vectors, complex
637640
remove_returns(goto_model);

‎jbmc/src/janalyzer/janalyzer_parse_options.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,6 @@ class janalyzer_parse_optionst : public parse_options_baset
159159
janalyzer_parse_optionst(int argc, const char **argv);
160160

161161
protected:
162-
ui_message_handlert ui_message_handler;
163162
goto_modelt goto_model;
164163

165164
void register_languages();
@@ -174,7 +173,7 @@ class janalyzer_parse_optionst : public parse_options_baset
174173

175174
ui_message_handlert::uit get_ui()
176175
{
177-
return ui_message_handler.get_ui();
176+
return message_handler->get_ui();
178177
}
179178
};
180179

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 39 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,11 @@ Author: Daniel Kroening, [email protected]
7777
#include <java_bytecode/simple_method_stubbing.h>
7878

7979
jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
80-
: parse_options_baset(JBMC_OPTIONS, argc, argv, ui_message_handler),
81-
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
80+
: parse_options_baset(
81+
JBMC_OPTIONS,
82+
argc,
83+
argv,
84+
std::string("JBMC ") + CBMC_VERSION)
8285
{
8386
}
8487

@@ -90,8 +93,7 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
9093
JBMC_OPTIONS + extra_options,
9194
argc,
9295
argv,
93-
ui_message_handler),
94-
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
96+
std::string("JBMC ") + CBMC_VERSION)
9597
{
9698
}
9799

@@ -158,7 +160,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
158160
if(
159161
cmdline.isset("trace") || cmdline.isset("compact-trace") ||
160162
cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
161-
(ui_message_handler.get_ui() != ui_message_handlert::uit::PLAIN &&
163+
(message_handler->get_ui() != ui_message_handlert::uit::PLAIN &&
162164
!cmdline.isset("cover")))
163165
{
164166
options.set_option("trace", true);
@@ -442,7 +444,7 @@ int jbmc_parse_optionst::doit()
442444
<< config.this_operating_system() << messaget::eom;
443445

444446
// output the options
445-
switch(ui_message_handler.get_ui())
447+
switch(message_handler->get_ui())
446448
{
447449
case ui_message_handlert::uit::PLAIN:
448450
log.conditional_output(
@@ -564,7 +566,7 @@ int jbmc_parse_optionst::doit()
564566
if(cmdline.isset("show-properties"))
565567
{
566568
show_properties(
567-
goto_model, log.get_message_handler(), ui_message_handler.get_ui());
569+
goto_model, log.get_message_handler(), message_handler->get_ui());
568570
return 0; // should contemplate EX_OK from sysexits.h
569571
}
570572

@@ -578,13 +580,13 @@ int jbmc_parse_optionst::doit()
578580
if(options.get_bool_option("paths"))
579581
{
580582
all_properties_verifiert<java_single_path_symex_only_checkert> verifier(
581-
options, ui_message_handler, goto_model);
583+
options, *message_handler, goto_model);
582584
(void)verifier();
583585
}
584586
else
585587
{
586588
all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
587-
options, ui_message_handler, goto_model);
589+
options, *message_handler, goto_model);
588590
(void)verifier();
589591
}
590592

@@ -598,13 +600,13 @@ int jbmc_parse_optionst::doit()
598600
if(options.get_bool_option("paths"))
599601
{
600602
stop_on_fail_verifiert<java_single_path_symex_checkert> verifier(
601-
options, ui_message_handler, goto_model);
603+
options, *message_handler, goto_model);
602604
(void)verifier();
603605
}
604606
else
605607
{
606608
stop_on_fail_verifiert<java_multi_path_symex_checkert> verifier(
607-
options, ui_message_handler, goto_model);
609+
options, *message_handler, goto_model);
608610
(void)verifier();
609611
}
610612

@@ -619,7 +621,7 @@ int jbmc_parse_optionst::doit()
619621
{
620622
verifier = util_make_unique<
621623
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
622-
options, ui_message_handler, goto_model);
624+
options, *message_handler, goto_model);
623625
}
624626
else if(
625627
options.get_bool_option("stop-on-fail") &&
@@ -630,13 +632,13 @@ int jbmc_parse_optionst::doit()
630632
verifier =
631633
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
632634
java_multi_path_symex_checkert>>(
633-
options, ui_message_handler, goto_model);
635+
options, *message_handler, goto_model);
634636
}
635637
else
636638
{
637639
verifier = util_make_unique<
638640
stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
639-
options, ui_message_handler, goto_model);
641+
options, *message_handler, goto_model);
640642
}
641643
}
642644
else if(
@@ -645,7 +647,7 @@ int jbmc_parse_optionst::doit()
645647
{
646648
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
647649
java_single_path_symex_checkert>>(
648-
options, ui_message_handler, goto_model);
650+
options, *message_handler, goto_model);
649651
}
650652
else if(
651653
!options.get_bool_option("stop-on-fail") &&
@@ -656,13 +658,13 @@ int jbmc_parse_optionst::doit()
656658
verifier =
657659
util_make_unique<all_properties_verifier_with_fault_localizationt<
658660
java_multi_path_symex_checkert>>(
659-
options, ui_message_handler, goto_model);
661+
options, *message_handler, goto_model);
660662
}
661663
else
662664
{
663665
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
664666
java_multi_path_symex_checkert>>(
665-
options, ui_message_handler, goto_model);
667+
options, *message_handler, goto_model);
666668
}
667669
}
668670
else
@@ -672,7 +674,7 @@ int jbmc_parse_optionst::doit()
672674
// The `configure_bmc` callback passed will enable enum-unwind-static if
673675
// applicable.
674676
return bmct::do_language_agnostic_bmc(
675-
options, goto_model, ui_message_handler, configure_bmc);
677+
options, goto_model, *message_handler, configure_bmc);
676678
}
677679

678680
const resultt result = (*verifier)();
@@ -683,7 +685,7 @@ int jbmc_parse_optionst::doit()
683685
{
684686
// Use symex-driven lazy loading:
685687
lazy_goto_modelt lazy_goto_model =
686-
lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler);
688+
lazy_goto_modelt::from_handler_object(*this, options, *message_handler);
687689
lazy_goto_model.initialize(cmdline.args, options);
688690

689691
class_hierarchy =
@@ -720,7 +722,7 @@ int jbmc_parse_optionst::doit()
720722
return bmct::do_language_agnostic_bmc(
721723
options,
722724
lazy_goto_model,
723-
ui_message_handler,
725+
*message_handler,
724726
configure_bmc,
725727
callback_after_symex);
726728
}
@@ -740,7 +742,7 @@ int jbmc_parse_optionst::get_goto_program(
740742
{
741743
{
742744
lazy_goto_modelt lazy_goto_model =
743-
lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler);
745+
lazy_goto_modelt::from_handler_object(*this, options, *message_handler);
744746
lazy_goto_model.initialize(cmdline.args, options);
745747

746748
class_hierarchy =
@@ -749,7 +751,7 @@ int jbmc_parse_optionst::get_goto_program(
749751
// Show the class hierarchy
750752
if(cmdline.isset("show-class-hierarchy"))
751753
{
752-
show_class_hierarchy(*class_hierarchy, ui_message_handler);
754+
show_class_hierarchy(*class_hierarchy, *message_handler);
753755
return CPROVER_EXIT_SUCCESS;
754756
}
755757

@@ -764,12 +766,12 @@ int jbmc_parse_optionst::get_goto_program(
764766
// values, etc
765767
if(cmdline.isset("show-symbol-table"))
766768
{
767-
show_symbol_table(lazy_goto_model.symbol_table, ui_message_handler);
769+
show_symbol_table(lazy_goto_model.symbol_table, *message_handler);
768770
return 0;
769771
}
770772
else if(cmdline.isset("list-symbols"))
771773
{
772-
show_symbol_table_brief(lazy_goto_model.symbol_table, ui_message_handler);
774+
show_symbol_table_brief(lazy_goto_model.symbol_table, *message_handler);
773775
return 0;
774776
}
775777

@@ -788,7 +790,7 @@ int jbmc_parse_optionst::get_goto_program(
788790
// show it?
789791
if(cmdline.isset("show-loops"))
790792
{
791-
show_loop_ids(ui_message_handler.get_ui(), *goto_model);
793+
show_loop_ids(message_handler->get_ui(), *goto_model);
792794
return 0;
793795
}
794796

@@ -800,7 +802,7 @@ int jbmc_parse_optionst::get_goto_program(
800802
show_goto_functions(
801803
*goto_model,
802804
log.get_message_handler(),
803-
ui_message_handler.get_ui(),
805+
message_handler->get_ui(),
804806
cmdline.isset("list-goto-functions"));
805807
return 0;
806808
}
@@ -844,8 +846,7 @@ void jbmc_parse_optionst::process_goto_function(
844846
replace_java_nondet(function);
845847

846848
// Similar removal of java nondet statements:
847-
convert_nondet(
848-
function, ui_message_handler, object_factory_params, ID_java);
849+
convert_nondet(function, *message_handler, object_factory_params, ID_java);
849850

850851
if(using_symex_driven_loading)
851852
{
@@ -859,7 +860,7 @@ void jbmc_parse_optionst::process_goto_function(
859860
goto_function.body,
860861
symbol_table,
861862
*class_hierarchy.get(),
862-
ui_message_handler);
863+
*message_handler);
863864
}
864865

865866
// add generic checks
@@ -871,7 +872,7 @@ void jbmc_parse_optionst::process_goto_function(
871872
function.get_function_id(),
872873
goto_function,
873874
symbol_table,
874-
ui_message_handler);
875+
*message_handler);
875876

876877
// checks don't know about adjusted float expressions
877878
adjust_float_expressions(goto_function, ns);
@@ -908,18 +909,18 @@ bool jbmc_parse_optionst::show_loaded_functions(
908909
{
909910
if(cmdline.isset("show-symbol-table"))
910911
{
911-
show_symbol_table(goto_model.get_symbol_table(), ui_message_handler);
912+
show_symbol_table(goto_model.get_symbol_table(), *message_handler);
912913
return true;
913914
}
914915
else if(cmdline.isset("list-symbols"))
915916
{
916-
show_symbol_table_brief(goto_model.get_symbol_table(), ui_message_handler);
917+
show_symbol_table_brief(goto_model.get_symbol_table(), *message_handler);
917918
return true;
918919
}
919920

920921
if(cmdline.isset("show-loops"))
921922
{
922-
show_loop_ids(ui_message_handler.get_ui(), goto_model.get_goto_functions());
923+
show_loop_ids(message_handler->get_ui(), goto_model.get_goto_functions());
923924
return true;
924925
}
925926

@@ -930,8 +931,8 @@ bool jbmc_parse_optionst::show_loaded_functions(
930931
namespacet ns(goto_model.get_symbol_table());
931932
show_goto_functions(
932933
ns,
933-
ui_message_handler,
934-
ui_message_handler.get_ui(),
934+
*message_handler,
935+
message_handler->get_ui(),
935936
goto_model.get_goto_functions(),
936937
cmdline.isset("list-goto-functions"));
937938
return true;
@@ -943,7 +944,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
943944
show_properties(
944945
ns,
945946
log.get_message_handler(),
946-
ui_message_handler.get_ui(),
947+
message_handler->get_ui(),
947948
goto_model.get_goto_functions());
948949
return true;
949950
}
@@ -1077,9 +1078,9 @@ bool jbmc_parse_optionst::generate_function_body(
10771078
symbol_table,
10781079
stub_objects_are_not_null,
10791080
object_factory_params,
1080-
ui_message_handler);
1081+
*message_handler);
10811082

1082-
goto_convert_functionst converter(symbol_table, ui_message_handler);
1083+
goto_convert_functionst converter(symbol_table, *message_handler);
10831084
converter.convert_function(function_name, function);
10841085

10851086
return true;

‎jbmc/src/jbmc/jbmc_parse_options.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,6 @@ class jbmc_parse_optionst : public parse_options_baset
117117
bool body_available);
118118

119119
protected:
120-
ui_message_handlert ui_message_handler;
121120
java_object_factory_parameterst object_factory_params;
122121
bool stub_objects_are_not_null;
123122

0 commit comments

Comments
 (0)