Remove obsolete cbmc/fault_localization

The goto-checker infrastructure is used now.

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -42,7 +42,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
       # Empty last line
 
 INCLUDES= -I .. -I ../$(CPROVER_DIR)/src

src/cbmc/Makefile

@@ -5,7 +5,6 @@ SRC = all_properties.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \
-      fault_localization.cpp \
       xml_interface.cpp \
       # Empty last line
 

src/cbmc/bmc.cpp

@@ -29,8 +29,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/report_util.h>
 #include <goto-checker/solver_factory.h>
 
-#include "fault_localization.h"
-
 /// Hook used by CEGIS to selectively freeze variables
 /// in the SAT solver after the SSA formula is added to the solver.
 /// Freezing variables is necessary to make use of incremental
@@ -139,13 +137,6 @@ safety_checkert::resultt bmct::execute(
         safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
     }
 
-    if(options.get_option("localize-faults")!="")
-    {
-      fault_localizationt fault_localization(
-        goto_functions, *this, options);
-      return fault_localization();
-    }
-
     // any properties to check at all?
     if(
       !options.get_bool_option("program-only") &&

src/cbmc/bmc.h

@@ -197,7 +197,6 @@ class bmct:public safety_checkert
   friend class bmc_covert;
   template <template <class goalt> class covert>
   friend class bmc_goal_covert;
-  friend class fault_localizationt;
 
 private:
   /// \brief Class-specific symbolic execution