Skip to content

Commit 87d0a5a

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 326f958 commit 87d0a5a

19 files changed

+152
-134
lines changed

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,13 @@ 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+
util_make_unique<ui_message_handlert>(
66+
cmdline,
67+
std::string("JANALYZER ") + CBMC_VERSION))
6368
{
6469
}
6570

@@ -344,7 +349,7 @@ int janalyzer_parse_optionst::doit()
344349
optionst options;
345350
get_command_line_options(options);
346351
messaget::eval_verbosity(
347-
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
352+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, *message_handler);
348353

349354
//
350355
// Print a banner
@@ -377,7 +382,7 @@ int janalyzer_parse_optionst::doit()
377382
// show it?
378383
if(cmdline.isset("show-symbol-table"))
379384
{
380-
::show_symbol_table(goto_model.symbol_table, ui_message_handler);
385+
::show_symbol_table(goto_model.symbol_table, *message_handler);
381386
return CPROVER_EXIT_SUCCESS;
382387
}
383388

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

632637
// do partial inlining
633638
log.status() << "Partial Inlining" << messaget::eom;
634-
goto_partial_inline(goto_model, ui_message_handler);
639+
goto_partial_inline(goto_model, *message_handler);
635640

636641
// remove returns, gcc vectors, complex
637642
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: 43 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,13 @@ 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+
util_make_unique<ui_message_handlert>(
85+
cmdline,
86+
std::string("JBMC ") + CBMC_VERSION))
8287
{
8388
}
8489

@@ -90,8 +95,9 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
9095
JBMC_OPTIONS + extra_options,
9196
argc,
9297
argv,
93-
ui_message_handler),
94-
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
98+
util_make_unique<ui_message_handlert>(
99+
cmdline,
100+
std::string("JBMC ") + CBMC_VERSION))
95101
{
96102
}
97103

@@ -158,7 +164,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
158164
if(
159165
cmdline.isset("trace") || cmdline.isset("compact-trace") ||
160166
cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
161-
(ui_message_handler.get_ui() != ui_message_handlert::uit::PLAIN &&
167+
(message_handler->get_ui() != ui_message_handlert::uit::PLAIN &&
162168
!cmdline.isset("cover")))
163169
{
164170
options.set_option("trace", true);
@@ -442,7 +448,7 @@ int jbmc_parse_optionst::doit()
442448
<< config.this_operating_system() << messaget::eom;
443449

444450
// output the options
445-
switch(ui_message_handler.get_ui())
451+
switch(message_handler->get_ui())
446452
{
447453
case ui_message_handlert::uit::PLAIN:
448454
log.conditional_output(
@@ -566,7 +572,7 @@ int jbmc_parse_optionst::doit()
566572
if(cmdline.isset("show-properties"))
567573
{
568574
show_properties(
569-
goto_model, log.get_message_handler(), ui_message_handler.get_ui());
575+
goto_model, log.get_message_handler(), message_handler->get_ui());
570576
return 0; // should contemplate EX_OK from sysexits.h
571577
}
572578

@@ -580,13 +586,13 @@ int jbmc_parse_optionst::doit()
580586
if(options.get_bool_option("paths"))
581587
{
582588
all_properties_verifiert<java_single_path_symex_only_checkert> verifier(
583-
options, ui_message_handler, goto_model);
589+
options, *message_handler, goto_model);
584590
(void)verifier();
585591
}
586592
else
587593
{
588594
all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
589-
options, ui_message_handler, goto_model);
595+
options, *message_handler, goto_model);
590596
(void)verifier();
591597
}
592598

@@ -600,13 +606,13 @@ int jbmc_parse_optionst::doit()
600606
if(options.get_bool_option("paths"))
601607
{
602608
stop_on_fail_verifiert<java_single_path_symex_checkert> verifier(
603-
options, ui_message_handler, goto_model);
609+
options, *message_handler, goto_model);
604610
(void)verifier();
605611
}
606612
else
607613
{
608614
stop_on_fail_verifiert<java_multi_path_symex_checkert> verifier(
609-
options, ui_message_handler, goto_model);
615+
options, *message_handler, goto_model);
610616
(void)verifier();
611617
}
612618

@@ -621,7 +627,7 @@ int jbmc_parse_optionst::doit()
621627
{
622628
verifier = util_make_unique<
623629
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
624-
options, ui_message_handler, goto_model);
630+
options, *message_handler, goto_model);
625631
}
626632
else if(
627633
options.get_bool_option("stop-on-fail") &&
@@ -632,13 +638,13 @@ int jbmc_parse_optionst::doit()
632638
verifier =
633639
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
634640
java_multi_path_symex_checkert>>(
635-
options, ui_message_handler, goto_model);
641+
options, *message_handler, goto_model);
636642
}
637643
else
638644
{
639645
verifier = util_make_unique<
640646
stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
641-
options, ui_message_handler, goto_model);
647+
options, *message_handler, goto_model);
642648
}
643649
}
644650
else if(
@@ -647,7 +653,7 @@ int jbmc_parse_optionst::doit()
647653
{
648654
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
649655
java_single_path_symex_checkert>>(
650-
options, ui_message_handler, goto_model);
656+
options, *message_handler, goto_model);
651657
}
652658
else if(
653659
!options.get_bool_option("stop-on-fail") &&
@@ -658,13 +664,13 @@ int jbmc_parse_optionst::doit()
658664
verifier =
659665
util_make_unique<all_properties_verifier_with_fault_localizationt<
660666
java_multi_path_symex_checkert>>(
661-
options, ui_message_handler, goto_model);
667+
options, *message_handler, goto_model);
662668
}
663669
else
664670
{
665671
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
666672
java_multi_path_symex_checkert>>(
667-
options, ui_message_handler, goto_model);
673+
options, *message_handler, goto_model);
668674
}
669675
}
670676
else
@@ -674,7 +680,7 @@ int jbmc_parse_optionst::doit()
674680
// The `configure_bmc` callback passed will enable enum-unwind-static if
675681
// applicable.
676682
return bmct::do_language_agnostic_bmc(
677-
options, goto_model, ui_message_handler, configure_bmc);
683+
options, goto_model, *message_handler, configure_bmc);
678684
}
679685

680686
const resultt result = (*verifier)();
@@ -685,7 +691,7 @@ int jbmc_parse_optionst::doit()
685691
{
686692
// Use symex-driven lazy loading:
687693
lazy_goto_modelt lazy_goto_model =
688-
lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler);
694+
lazy_goto_modelt::from_handler_object(*this, options, *message_handler);
689695
lazy_goto_model.initialize(cmdline.args, options);
690696

691697
class_hierarchy =
@@ -722,7 +728,7 @@ int jbmc_parse_optionst::doit()
722728
return bmct::do_language_agnostic_bmc(
723729
options,
724730
lazy_goto_model,
725-
ui_message_handler,
731+
*message_handler,
726732
configure_bmc,
727733
callback_after_symex);
728734
}
@@ -742,7 +748,7 @@ int jbmc_parse_optionst::get_goto_program(
742748
{
743749
{
744750
lazy_goto_modelt lazy_goto_model =
745-
lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler);
751+
lazy_goto_modelt::from_handler_object(*this, options, *message_handler);
746752
lazy_goto_model.initialize(cmdline.args, options);
747753

748754
class_hierarchy =
@@ -751,7 +757,7 @@ int jbmc_parse_optionst::get_goto_program(
751757
// Show the class hierarchy
752758
if(cmdline.isset("show-class-hierarchy"))
753759
{
754-
show_class_hierarchy(*class_hierarchy, ui_message_handler);
760+
show_class_hierarchy(*class_hierarchy, *message_handler);
755761
return CPROVER_EXIT_SUCCESS;
756762
}
757763

@@ -766,12 +772,12 @@ int jbmc_parse_optionst::get_goto_program(
766772
// values, etc
767773
if(cmdline.isset("show-symbol-table"))
768774
{
769-
show_symbol_table(lazy_goto_model.symbol_table, ui_message_handler);
775+
show_symbol_table(lazy_goto_model.symbol_table, *message_handler);
770776
return 0;
771777
}
772778
else if(cmdline.isset("list-symbols"))
773779
{
774-
show_symbol_table_brief(lazy_goto_model.symbol_table, ui_message_handler);
780+
show_symbol_table_brief(lazy_goto_model.symbol_table, *message_handler);
775781
return 0;
776782
}
777783

@@ -790,7 +796,7 @@ int jbmc_parse_optionst::get_goto_program(
790796
// show it?
791797
if(cmdline.isset("show-loops"))
792798
{
793-
show_loop_ids(ui_message_handler.get_ui(), *goto_model);
799+
show_loop_ids(message_handler->get_ui(), *goto_model);
794800
return 0;
795801
}
796802

@@ -802,7 +808,7 @@ int jbmc_parse_optionst::get_goto_program(
802808
show_goto_functions(
803809
*goto_model,
804810
log.get_message_handler(),
805-
ui_message_handler.get_ui(),
811+
message_handler->get_ui(),
806812
cmdline.isset("list-goto-functions"));
807813
return 0;
808814
}
@@ -846,8 +852,7 @@ void jbmc_parse_optionst::process_goto_function(
846852
replace_java_nondet(function);
847853

848854
// Similar removal of java nondet statements:
849-
convert_nondet(
850-
function, ui_message_handler, object_factory_params, ID_java);
855+
convert_nondet(function, *message_handler, object_factory_params, ID_java);
851856

852857
if(using_symex_driven_loading)
853858
{
@@ -861,7 +866,7 @@ void jbmc_parse_optionst::process_goto_function(
861866
goto_function.body,
862867
symbol_table,
863868
*class_hierarchy.get(),
864-
ui_message_handler);
869+
*message_handler);
865870
}
866871

867872
// add generic checks
@@ -873,7 +878,7 @@ void jbmc_parse_optionst::process_goto_function(
873878
function.get_function_id(),
874879
goto_function,
875880
symbol_table,
876-
ui_message_handler);
881+
*message_handler);
877882

878883
// checks don't know about adjusted float expressions
879884
adjust_float_expressions(goto_function, ns);
@@ -910,18 +915,18 @@ bool jbmc_parse_optionst::show_loaded_functions(
910915
{
911916
if(cmdline.isset("show-symbol-table"))
912917
{
913-
show_symbol_table(goto_model.get_symbol_table(), ui_message_handler);
918+
show_symbol_table(goto_model.get_symbol_table(), *message_handler);
914919
return true;
915920
}
916921
else if(cmdline.isset("list-symbols"))
917922
{
918-
show_symbol_table_brief(goto_model.get_symbol_table(), ui_message_handler);
923+
show_symbol_table_brief(goto_model.get_symbol_table(), *message_handler);
919924
return true;
920925
}
921926

922927
if(cmdline.isset("show-loops"))
923928
{
924-
show_loop_ids(ui_message_handler.get_ui(), goto_model.get_goto_functions());
929+
show_loop_ids(message_handler->get_ui(), goto_model.get_goto_functions());
925930
return true;
926931
}
927932

@@ -932,8 +937,8 @@ bool jbmc_parse_optionst::show_loaded_functions(
932937
namespacet ns(goto_model.get_symbol_table());
933938
show_goto_functions(
934939
ns,
935-
ui_message_handler,
936-
ui_message_handler.get_ui(),
940+
*message_handler,
941+
message_handler->get_ui(),
937942
goto_model.get_goto_functions(),
938943
cmdline.isset("list-goto-functions"));
939944
return true;
@@ -945,7 +950,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
945950
show_properties(
946951
ns,
947952
log.get_message_handler(),
948-
ui_message_handler.get_ui(),
953+
message_handler->get_ui(),
949954
goto_model.get_goto_functions());
950955
return true;
951956
}
@@ -1079,9 +1084,9 @@ bool jbmc_parse_optionst::generate_function_body(
10791084
symbol_table,
10801085
stub_objects_are_not_null,
10811086
object_factory_params,
1082-
ui_message_handler);
1087+
*message_handler);
10831088

1084-
goto_convert_functionst converter(symbol_table, ui_message_handler);
1089+
goto_convert_functionst converter(symbol_table, *message_handler);
10851090
converter.convert_function(function_name, function);
10861091

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