Skip to content

Commit f157b2b

Browse files
peterschrammelpeterschrammel
committed
Refactor goto verifier selection
reduces indentation
1 parent 7f3c681 commit f157b2b

File tree

2 files changed

+91
-105
lines changed

2 files changed

+91
-105
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 47 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -596,73 +596,68 @@ int jbmc_parse_optionst::doit()
596596
std::unique_ptr<goto_verifiert> verifier = nullptr;
597597

598598
if(
599-
!options.is_set("cover") && !options.get_bool_option("dimacs") &&
600-
options.get_option("outfile").empty())
599+
options.get_bool_option("stop-on-fail") &&
600+
options.get_bool_option("paths"))
601601
{
602-
if(options.get_bool_option("stop-on-fail"))
602+
verifier = util_make_unique<
603+
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
604+
options, ui_message_handler, goto_model);
605+
}
606+
else if(
607+
options.get_bool_option("stop-on-fail") &&
608+
!options.get_bool_option("paths"))
609+
{
610+
if(options.get_bool_option("localize-faults"))
603611
{
604-
if(options.get_bool_option("paths"))
605-
{
606-
verifier = util_make_unique<
607-
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
612+
verifier =
613+
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
614+
java_multi_path_symex_checkert>>(
608615
options, ui_message_handler, goto_model);
609-
}
610-
else
611-
{
612-
if(options.get_bool_option("localize-faults"))
613-
{
614-
verifier =
615-
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
616-
java_multi_path_symex_checkert>>(
617-
options, ui_message_handler, goto_model);
618-
}
619-
else
620-
{
621-
verifier = util_make_unique<
622-
stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
623-
options, ui_message_handler, goto_model);
624-
}
625-
}
626616
}
627617
else
628618
{
629-
if(options.get_bool_option("paths"))
630-
{
631-
verifier =
632-
util_make_unique<all_properties_verifier_with_trace_storaget<
633-
java_single_path_symex_checkert>>(
634-
options, ui_message_handler, goto_model);
635-
}
636-
else
637-
{
638-
if(options.get_bool_option("localize-faults"))
639-
{
640-
verifier =
641-
util_make_unique<all_properties_verifier_with_fault_localizationt<
642-
java_multi_path_symex_checkert>>(
643-
options, ui_message_handler, goto_model);
644-
}
645-
else
646-
{
647-
verifier =
648-
util_make_unique<all_properties_verifier_with_trace_storaget<
649-
java_multi_path_symex_checkert>>(
650-
options, ui_message_handler, goto_model);
651-
}
652-
}
619+
verifier = util_make_unique<
620+
stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
621+
options, ui_message_handler, goto_model);
653622
}
654623
}
655-
656-
// fall back until everything has been ported to goto-checker
657-
if(verifier == nullptr)
624+
else if(
625+
!options.get_bool_option("stop-on-fail") &&
626+
options.get_bool_option("paths"))
658627
{
628+
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
629+
java_single_path_symex_checkert>>(
630+
options, ui_message_handler, goto_model);
631+
}
632+
else if(
633+
!options.get_bool_option("stop-on-fail") &&
634+
!options.get_bool_option("paths"))
635+
{
636+
if(options.get_bool_option("localize-faults"))
637+
{
638+
verifier =
639+
util_make_unique<all_properties_verifier_with_fault_localizationt<
640+
java_multi_path_symex_checkert>>(
641+
options, ui_message_handler, goto_model);
642+
}
643+
else
644+
{
645+
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
646+
java_multi_path_symex_checkert>>(
647+
options, ui_message_handler, goto_model);
648+
}
649+
}
650+
else
651+
{
652+
// fall back until everything has been ported to goto-checker
653+
659654
// The `configure_bmc` callback passed will enable enum-unwind-static if
660655
// applicable.
661656
return bmct::do_language_agnostic_bmc(
662657
options, goto_model, ui_message_handler, configure_bmc);
663658
}
664659

665-
resultt result = (*verifier)();
660+
const resultt result = (*verifier)();
666661
verifier->report();
667662
return result_to_exit_code(result);
668663
}

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 44 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -608,69 +608,60 @@ int cbmc_parse_optionst::doit()
608608
std::unique_ptr<goto_verifiert> verifier = nullptr;
609609

610610
if(
611-
!options.is_set("cover") && !options.get_bool_option("dimacs") &&
612-
options.get_option("outfile").empty())
611+
options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
613612
{
614-
if(options.get_bool_option("stop-on-fail"))
613+
verifier =
614+
util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
615+
options, ui_message_handler, goto_model);
616+
}
617+
else if(
618+
options.get_bool_option("stop-on-fail") &&
619+
!options.get_bool_option("paths"))
620+
{
621+
if(options.get_bool_option("localize-faults"))
615622
{
616-
if(options.get_bool_option("paths"))
617-
{
618-
verifier =
619-
util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
620-
options, ui_message_handler, goto_model);
621-
}
622-
else
623-
{
624-
if(options.get_bool_option("localize-faults"))
625-
{
626-
verifier =
627-
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
628-
multi_path_symex_checkert>>(
629-
options, ui_message_handler, goto_model);
630-
}
631-
else
632-
{
633-
verifier =
634-
util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
635-
options, ui_message_handler, goto_model);
636-
}
637-
}
623+
verifier =
624+
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
625+
multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
638626
}
639627
else
640628
{
641-
if(options.get_bool_option("paths"))
642-
{
643-
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
644-
single_path_symex_checkert>>(options, ui_message_handler, goto_model);
645-
}
646-
else
647-
{
648-
if(options.get_bool_option("localize-faults"))
649-
{
650-
verifier =
651-
util_make_unique<all_properties_verifier_with_fault_localizationt<
652-
multi_path_symex_checkert>>(
653-
options, ui_message_handler, goto_model);
654-
}
655-
else
656-
{
657-
verifier =
658-
util_make_unique<all_properties_verifier_with_trace_storaget<
659-
multi_path_symex_checkert>>(
660-
options, ui_message_handler, goto_model);
661-
}
662-
}
629+
verifier =
630+
util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
631+
options, ui_message_handler, goto_model);
663632
}
664633
}
665-
666-
// fall back until everything has been ported to goto-checker
667-
if(verifier == nullptr)
634+
else if(
635+
!options.get_bool_option("stop-on-fail") &&
636+
options.get_bool_option("paths"))
637+
{
638+
verifier = util_make_unique<
639+
all_properties_verifier_with_trace_storaget<single_path_symex_checkert>>(
640+
options, ui_message_handler, goto_model);
641+
}
642+
else if(
643+
!options.get_bool_option("stop-on-fail") &&
644+
!options.get_bool_option("paths"))
645+
{
646+
if(options.get_bool_option("localize-faults"))
647+
{
648+
verifier =
649+
util_make_unique<all_properties_verifier_with_fault_localizationt<
650+
multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
651+
}
652+
else
653+
{
654+
verifier = util_make_unique<
655+
all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
656+
options, ui_message_handler, goto_model);
657+
}
658+
}
659+
else
668660
{
669-
return bmct::do_language_agnostic_bmc(
670-
options, goto_model, ui_message_handler);
661+
UNREACHABLE;
671662
}
672663

673-
resultt result = (*verifier)();
664+
const resultt result = (*verifier)();
674665
verifier->report();
675666

676667
return result_to_exit_code(result);

0 commit comments

Comments
 (0)