Skip to content

Commit ce69f1d

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #4215 from peterschrammel/remove-bmct-fault-localization
Remove obsolete cbmc/fault_localization [blocks: 4216]
2 parents 141223a + d9b910b commit ce69f1d

File tree

11 files changed

+91
-642
lines changed

11 files changed

+91
-642
lines changed

‎jbmc/src/jbmc/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
4242
../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
4343
../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
4444
../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
45-
../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
4645
# Empty last line
4746

4847
INCLUDES= -I .. -I ../$(CPROVER_DIR)/src

‎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
}

‎jbmc/unit/Makefile

Lines changed: 0 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -82,24 +82,6 @@ java-testing-utils/java-testing-utils$(LIBEXT): jprover.dir
8282
java-testing-utils-clean:
8383
$(MAKE) $(MAKEARGS) -C java-testing-utils clean
8484

85-
# We need to link bmc.o to the unit test, so here's everything it depends on...
86-
BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
87-
$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
88-
$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
89-
$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
90-
$(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \
91-
$(CPROVER_DIR)/src/jsil/jsil_convert$(OBJEXT) \
92-
$(CPROVER_DIR)/src/jsil/jsil_entry_point$(OBJEXT) \
93-
$(CPROVER_DIR)/src/jsil/jsil_internal_additions$(OBJEXT) \
94-
$(CPROVER_DIR)/src/jsil/jsil_language$(OBJEXT) \
95-
$(CPROVER_DIR)/src/jsil/jsil_lex.yy$(OBJEXT) \
96-
$(CPROVER_DIR)/src/jsil/jsil_parser$(OBJEXT) \
97-
$(CPROVER_DIR)/src/jsil/jsil_parse_tree$(OBJEXT) \
98-
$(CPROVER_DIR)/src/jsil/jsil_typecheck$(OBJEXT) \
99-
$(CPROVER_DIR)/src/jsil/jsil_types$(OBJEXT) \
100-
$(CPROVER_DIR)/src/jsil/jsil_y.tab$(OBJEXT) \
101-
# Empty last line
102-
10385
CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
10486
../src/miniz/miniz$(OBJEXT) \
10587
$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
@@ -133,7 +115,6 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
133115
$(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \
134116
$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
135117
$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
136-
$(BMC_DEPS) \
137118
# Empty last line
138119

139120
OBJ += $(CPROVER_LIBS) \

‎src/cbmc/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ SRC = all_properties.cpp \
55
cbmc_languages.cpp \
66
cbmc_main.cpp \
77
cbmc_parse_options.cpp \
8-
fault_localization.cpp \
98
xml_interface.cpp \
109
# Empty last line
1110

‎src/cbmc/bmc.cpp

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,6 @@ Author: Daniel Kroening, [email protected]
2929
#include <goto-checker/report_util.h>
3030
#include <goto-checker/solver_factory.h>
3131

32-
#include "fault_localization.h"
33-
3432
/// Hook used by CEGIS to selectively freeze variables
3533
/// in the SAT solver after the SSA formula is added to the solver.
3634
/// Freezing variables is necessary to make use of incremental
@@ -139,13 +137,6 @@ safety_checkert::resultt bmct::execute(
139137
safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
140138
}
141139

142-
if(options.get_option("localize-faults")!="")
143-
{
144-
fault_localizationt fault_localization(
145-
goto_functions, *this, options);
146-
return fault_localization();
147-
}
148-
149140
// any properties to check at all?
150141
if(
151142
!options.get_bool_option("program-only") &&

‎src/cbmc/bmc.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -197,7 +197,6 @@ class bmct:public safety_checkert
197197
friend class bmc_covert;
198198
template <template <class goalt> class covert>
199199
friend class bmc_goal_covert;
200-
friend class fault_localizationt;
201200

202201
private:
203202
/// \brief Class-specific symbolic execution

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