Skip to content

Commit edfa668

Browse files
romainbrenguierromainbrenguier
committed
fixup! Make parse_options_baset the owner of message_handler
1 parent d2baea5 commit edfa668

13 files changed

+97
-93
lines changed

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -347,7 +347,7 @@ int janalyzer_parse_optionst::doit()
347347
optionst options;
348348
get_command_line_options(options);
349349
messaget::eval_verbosity(
350-
cmdline.get_value("verbosity"), messaget::M_STATISTICS, *message_handler);
350+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, message_handler);
351351

352352
//
353353
// Print a banner
@@ -380,7 +380,7 @@ int janalyzer_parse_optionst::doit()
380380
// show it?
381381
if(cmdline.isset("show-symbol-table"))
382382
{
383-
::show_symbol_table(goto_model.symbol_table, *message_handler);
383+
::show_symbol_table(goto_model.symbol_table, message_handler);
384384
return CPROVER_EXIT_SUCCESS;
385385
}
386386

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

635635
// do partial inlining
636636
log.status() << "Partial Inlining" << messaget::eom;
637-
goto_partial_inline(goto_model, *message_handler);
637+
goto_partial_inline(goto_model, message_handler);
638638

639639
// remove returns, gcc vectors, complex
640640
remove_returns(goto_model);

‎jbmc/src/janalyzer/janalyzer_parse_options.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,7 @@ class janalyzer_parse_optionst : public parse_options_baset
173173

174174
ui_message_handlert::uit get_ui()
175175
{
176-
return message_handler->get_ui();
176+
return message_handler.get_ui();
177177
}
178178
};
179179

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 33 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
160160
if(
161161
cmdline.isset("trace") || cmdline.isset("compact-trace") ||
162162
cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
163-
(message_handler->get_ui() != ui_message_handlert::uit::PLAIN &&
163+
(message_handler.get_ui() != ui_message_handlert::uit::PLAIN &&
164164
!cmdline.isset("cover")))
165165
{
166166
options.set_option("trace", true);
@@ -444,7 +444,7 @@ int jbmc_parse_optionst::doit()
444444
<< config.this_operating_system() << messaget::eom;
445445

446446
// output the options
447-
switch(message_handler->get_ui())
447+
switch(message_handler.get_ui())
448448
{
449449
case ui_message_handlert::uit::PLAIN:
450450
log.conditional_output(
@@ -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(), message_handler->get_ui());
569+
goto_model, log.get_message_handler(), message_handler.get_ui());
570570
return 0; // should contemplate EX_OK from sysexits.h
571571
}
572572

@@ -580,13 +580,13 @@ int jbmc_parse_optionst::doit()
580580
if(options.get_bool_option("paths"))
581581
{
582582
all_properties_verifiert<java_single_path_symex_only_checkert> verifier(
583-
options, *message_handler, goto_model);
583+
options, message_handler, goto_model);
584584
(void)verifier();
585585
}
586586
else
587587
{
588588
all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
589-
options, *message_handler, goto_model);
589+
options, message_handler, goto_model);
590590
(void)verifier();
591591
}
592592

@@ -600,13 +600,13 @@ int jbmc_parse_optionst::doit()
600600
if(options.get_bool_option("paths"))
601601
{
602602
stop_on_fail_verifiert<java_single_path_symex_checkert> verifier(
603-
options, *message_handler, goto_model);
603+
options, message_handler, goto_model);
604604
(void)verifier();
605605
}
606606
else
607607
{
608608
stop_on_fail_verifiert<java_multi_path_symex_checkert> verifier(
609-
options, *message_handler, goto_model);
609+
options, message_handler, goto_model);
610610
(void)verifier();
611611
}
612612

@@ -621,7 +621,7 @@ int jbmc_parse_optionst::doit()
621621
{
622622
verifier = util_make_unique<
623623
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
624-
options, *message_handler, goto_model);
624+
options, message_handler, goto_model);
625625
}
626626
else if(
627627
options.get_bool_option("stop-on-fail") &&
@@ -632,13 +632,13 @@ int jbmc_parse_optionst::doit()
632632
verifier =
633633
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
634634
java_multi_path_symex_checkert>>(
635-
options, *message_handler, goto_model);
635+
options, message_handler, goto_model);
636636
}
637637
else
638638
{
639639
verifier = util_make_unique<
640640
stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
641-
options, *message_handler, goto_model);
641+
options, message_handler, goto_model);
642642
}
643643
}
644644
else if(
@@ -647,7 +647,7 @@ int jbmc_parse_optionst::doit()
647647
{
648648
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
649649
java_single_path_symex_checkert>>(
650-
options, *message_handler, goto_model);
650+
options, message_handler, goto_model);
651651
}
652652
else if(
653653
!options.get_bool_option("stop-on-fail") &&
@@ -658,13 +658,13 @@ int jbmc_parse_optionst::doit()
658658
verifier =
659659
util_make_unique<all_properties_verifier_with_fault_localizationt<
660660
java_multi_path_symex_checkert>>(
661-
options, *message_handler, goto_model);
661+
options, message_handler, goto_model);
662662
}
663663
else
664664
{
665665
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
666666
java_multi_path_symex_checkert>>(
667-
options, *message_handler, goto_model);
667+
options, message_handler, goto_model);
668668
}
669669
}
670670
else
@@ -674,7 +674,7 @@ int jbmc_parse_optionst::doit()
674674
// The `configure_bmc` callback passed will enable enum-unwind-static if
675675
// applicable.
676676
return bmct::do_language_agnostic_bmc(
677-
options, goto_model, *message_handler, configure_bmc);
677+
options, goto_model, message_handler, configure_bmc);
678678
}
679679

680680
const resultt result = (*verifier)();
@@ -685,7 +685,7 @@ int jbmc_parse_optionst::doit()
685685
{
686686
// Use symex-driven lazy loading:
687687
lazy_goto_modelt lazy_goto_model =
688-
lazy_goto_modelt::from_handler_object(*this, options, *message_handler);
688+
lazy_goto_modelt::from_handler_object(*this, options, message_handler);
689689
lazy_goto_model.initialize(cmdline.args, options);
690690

691691
class_hierarchy =
@@ -722,7 +722,7 @@ int jbmc_parse_optionst::doit()
722722
return bmct::do_language_agnostic_bmc(
723723
options,
724724
lazy_goto_model,
725-
*message_handler,
725+
message_handler,
726726
configure_bmc,
727727
callback_after_symex);
728728
}
@@ -742,7 +742,7 @@ int jbmc_parse_optionst::get_goto_program(
742742
{
743743
{
744744
lazy_goto_modelt lazy_goto_model =
745-
lazy_goto_modelt::from_handler_object(*this, options, *message_handler);
745+
lazy_goto_modelt::from_handler_object(*this, options, message_handler);
746746
lazy_goto_model.initialize(cmdline.args, options);
747747

748748
class_hierarchy =
@@ -751,7 +751,7 @@ int jbmc_parse_optionst::get_goto_program(
751751
// Show the class hierarchy
752752
if(cmdline.isset("show-class-hierarchy"))
753753
{
754-
show_class_hierarchy(*class_hierarchy, *message_handler);
754+
show_class_hierarchy(*class_hierarchy, message_handler);
755755
return CPROVER_EXIT_SUCCESS;
756756
}
757757

@@ -766,12 +766,12 @@ int jbmc_parse_optionst::get_goto_program(
766766
// values, etc
767767
if(cmdline.isset("show-symbol-table"))
768768
{
769-
show_symbol_table(lazy_goto_model.symbol_table, *message_handler);
769+
show_symbol_table(lazy_goto_model.symbol_table, message_handler);
770770
return 0;
771771
}
772772
else if(cmdline.isset("list-symbols"))
773773
{
774-
show_symbol_table_brief(lazy_goto_model.symbol_table, *message_handler);
774+
show_symbol_table_brief(lazy_goto_model.symbol_table, message_handler);
775775
return 0;
776776
}
777777

@@ -790,7 +790,7 @@ int jbmc_parse_optionst::get_goto_program(
790790
// show it?
791791
if(cmdline.isset("show-loops"))
792792
{
793-
show_loop_ids(message_handler->get_ui(), *goto_model);
793+
show_loop_ids(message_handler.get_ui(), *goto_model);
794794
return 0;
795795
}
796796

@@ -802,7 +802,7 @@ int jbmc_parse_optionst::get_goto_program(
802802
show_goto_functions(
803803
*goto_model,
804804
log.get_message_handler(),
805-
message_handler->get_ui(),
805+
message_handler.get_ui(),
806806
cmdline.isset("list-goto-functions"));
807807
return 0;
808808
}
@@ -846,7 +846,7 @@ void jbmc_parse_optionst::process_goto_function(
846846
replace_java_nondet(function);
847847

848848
// Similar removal of java nondet statements:
849-
convert_nondet(function, *message_handler, object_factory_params, ID_java);
849+
convert_nondet(function, message_handler, object_factory_params, ID_java);
850850

851851
if(using_symex_driven_loading)
852852
{
@@ -860,7 +860,7 @@ void jbmc_parse_optionst::process_goto_function(
860860
goto_function.body,
861861
symbol_table,
862862
*class_hierarchy.get(),
863-
*message_handler);
863+
message_handler);
864864
}
865865

866866
// add generic checks
@@ -872,7 +872,7 @@ void jbmc_parse_optionst::process_goto_function(
872872
function.get_function_id(),
873873
goto_function,
874874
symbol_table,
875-
*message_handler);
875+
message_handler);
876876

877877
// checks don't know about adjusted float expressions
878878
adjust_float_expressions(goto_function, ns);
@@ -909,18 +909,18 @@ bool jbmc_parse_optionst::show_loaded_functions(
909909
{
910910
if(cmdline.isset("show-symbol-table"))
911911
{
912-
show_symbol_table(goto_model.get_symbol_table(), *message_handler);
912+
show_symbol_table(goto_model.get_symbol_table(), message_handler);
913913
return true;
914914
}
915915
else if(cmdline.isset("list-symbols"))
916916
{
917-
show_symbol_table_brief(goto_model.get_symbol_table(), *message_handler);
917+
show_symbol_table_brief(goto_model.get_symbol_table(), message_handler);
918918
return true;
919919
}
920920

921921
if(cmdline.isset("show-loops"))
922922
{
923-
show_loop_ids(message_handler->get_ui(), goto_model.get_goto_functions());
923+
show_loop_ids(message_handler.get_ui(), goto_model.get_goto_functions());
924924
return true;
925925
}
926926

@@ -931,8 +931,8 @@ bool jbmc_parse_optionst::show_loaded_functions(
931931
namespacet ns(goto_model.get_symbol_table());
932932
show_goto_functions(
933933
ns,
934-
*message_handler,
935-
message_handler->get_ui(),
934+
message_handler,
935+
message_handler.get_ui(),
936936
goto_model.get_goto_functions(),
937937
cmdline.isset("list-goto-functions"));
938938
return true;
@@ -944,7 +944,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
944944
show_properties(
945945
ns,
946946
log.get_message_handler(),
947-
message_handler->get_ui(),
947+
message_handler.get_ui(),
948948
goto_model.get_goto_functions());
949949
return true;
950950
}
@@ -1078,9 +1078,9 @@ bool jbmc_parse_optionst::generate_function_body(
10781078
symbol_table,
10791079
stub_objects_are_not_null,
10801080
object_factory_params,
1081-
*message_handler);
1081+
message_handler);
10821082

1083-
goto_convert_functionst converter(symbol_table, *message_handler);
1083+
goto_convert_functionst converter(symbol_table, message_handler);
10841084
converter.convert_function(function_name, function);
10851085

10861086
return true;

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,7 @@ int jdiff_parse_optionst::doit()
189189
optionst options;
190190
get_command_line_options(options);
191191
messaget::eval_verbosity(
192-
cmdline.get_value("verbosity"), messaget::M_STATISTICS, *message_handler);
192+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, message_handler);
193193

194194
//
195195
// Print a banner
@@ -207,18 +207,18 @@ int jdiff_parse_optionst::doit()
207207
register_languages();
208208

209209
goto_modelt goto_model1 =
210-
initialize_goto_model({cmdline.args[0]}, *message_handler, options);
210+
initialize_goto_model({cmdline.args[0]}, message_handler, options);
211211
if(process_goto_program(options, goto_model1))
212212
return CPROVER_EXIT_INTERNAL_ERROR;
213213
goto_modelt goto_model2 =
214-
initialize_goto_model({cmdline.args[1]}, *message_handler, options);
214+
initialize_goto_model({cmdline.args[1]}, message_handler, options);
215215
if(process_goto_program(options, goto_model2))
216216
return CPROVER_EXIT_INTERNAL_ERROR;
217217

218218
if(cmdline.isset("show-loops"))
219219
{
220-
show_loop_ids(message_handler->get_ui(), goto_model1);
221-
show_loop_ids(message_handler->get_ui(), goto_model2);
220+
show_loop_ids(message_handler.get_ui(), goto_model1);
221+
show_loop_ids(message_handler.get_ui(), goto_model2);
222222
return CPROVER_EXIT_SUCCESS;
223223
}
224224

@@ -229,12 +229,12 @@ int jdiff_parse_optionst::doit()
229229
show_goto_functions(
230230
goto_model1,
231231
log.get_message_handler(),
232-
message_handler->get_ui(),
232+
message_handler.get_ui(),
233233
cmdline.isset("list-goto-functions"));
234234
show_goto_functions(
235235
goto_model2,
236236
log.get_message_handler(),
237-
message_handler->get_ui(),
237+
message_handler.get_ui(),
238238
cmdline.isset("list-goto-functions"));
239239
return CPROVER_EXIT_SUCCESS;
240240
}
@@ -263,7 +263,7 @@ int jdiff_parse_optionst::doit()
263263
return CPROVER_EXIT_SUCCESS;
264264
}
265265

266-
java_syntactic_difft sd(goto_model1, goto_model2, options, *message_handler);
266+
java_syntactic_difft sd(goto_model1, goto_model2, options, message_handler);
267267
sd();
268268
sd.output_functions();
269269

0 commit comments

Comments
 (0)