Skip to content

Commit 1b72e9a

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

File tree

2 files changed

+105
-116
lines changed

2 files changed

+105
-116
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 55 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -596,73 +596,70 @@ 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"))
603-
{
604-
if(options.get_bool_option("paths"))
605-
{
606-
verifier = util_make_unique<
607-
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
608-
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-
}
626-
}
627-
else
628-
{
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-
}
653-
}
602+
verifier = util_make_unique<
603+
stop_on_fail_verifiert<java_single_path_symex_checkert>>(
604+
options, ui_message_handler, goto_model);
654605
}
655-
656-
// fall back until everything has been ported to goto-checker
657-
if(verifier == nullptr)
606+
else if(
607+
options.get_bool_option("stop-on-fail") &&
608+
!options.get_bool_option("paths") &&
609+
options.get_bool_option("localize-faults"))
610+
{
611+
verifier =
612+
util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
613+
java_multi_path_symex_checkert>>(
614+
options, ui_message_handler, goto_model);
615+
}
616+
else if(
617+
options.get_bool_option("stop-on-fail") &&
618+
!options.get_bool_option("paths") &&
619+
!options.get_bool_option("localize-faults"))
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+
else if(
626+
!options.get_bool_option("stop-on-fail") &&
627+
options.get_bool_option("paths"))
628+
{
629+
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
630+
java_single_path_symex_checkert>>(
631+
options, ui_message_handler, goto_model);
632+
}
633+
else if(
634+
!options.get_bool_option("stop-on-fail") &&
635+
!options.get_bool_option("paths") &&
636+
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 if(
644+
!options.get_bool_option("stop-on-fail") &&
645+
!options.get_bool_option("paths") &&
646+
!options.get_bool_option("localize-faults"))
658647
{
648+
verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
649+
java_multi_path_symex_checkert>>(
650+
options, ui_message_handler, goto_model);
651+
}
652+
else
653+
{
654+
// fall back until everything has been ported to goto-checker
655+
659656
// The `configure_bmc` callback passed will enable enum-unwind-static if
660657
// applicable.
661658
return bmct::do_language_agnostic_bmc(
662659
options, goto_model, ui_message_handler, configure_bmc);
663660
}
664661

665-
resultt result = (*verifier)();
662+
const resultt result = (*verifier)();
666663
verifier->report();
667664
return result_to_exit_code(result);
668665
}

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 50 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -608,69 +608,61 @@ 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"))
615-
{
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-
}
638-
}
639-
else
640-
{
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-
}
663-
}
613+
verifier =
614+
util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
615+
options, ui_message_handler, goto_model);
664616
}
665-
666-
// fall back until everything has been ported to goto-checker
667-
if(verifier == nullptr)
617+
else if(
618+
options.get_bool_option("stop-on-fail") &&
619+
!options.get_bool_option("paths") &&
620+
options.get_bool_option("localize-faults"))
621+
{
622+
verifier = util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
623+
multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
624+
}
625+
else if(
626+
options.get_bool_option("stop-on-fail") &&
627+
!options.get_bool_option("paths") &&
628+
!options.get_bool_option("localize-faults"))
629+
{
630+
verifier =
631+
util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
632+
options, ui_message_handler, goto_model);
633+
}
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+
options.get_bool_option("localize-faults"))
646+
{
647+
verifier =
648+
util_make_unique<all_properties_verifier_with_fault_localizationt<
649+
multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
650+
}
651+
else if(
652+
!options.get_bool_option("stop-on-fail") &&
653+
!options.get_bool_option("paths") &&
654+
!options.get_bool_option("localize-faults"))
655+
{
656+
verifier = util_make_unique<
657+
all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
658+
options, ui_message_handler, goto_model);
659+
}
660+
else
668661
{
669-
return bmct::do_language_agnostic_bmc(
670-
options, goto_model, ui_message_handler);
662+
UNREACHABLE;
671663
}
672664

673-
resultt result = (*verifier)();
665+
const resultt result = (*verifier)();
674666
verifier->report();
675667

676668
return result_to_exit_code(result);

0 commit comments

Comments
 (0)