Remove obsolete cbmc/bmc_cover

The goto-checker infrastructure is used now.

Author: peterschrammel

jbmc/src/jbmc/Makefile

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

src/cbmc/Makefile

@@ -1,6 +1,5 @@
 SRC = all_properties.cpp \
       bmc.cpp \
-      bmc_cover.cpp \
       c_test_input_generator.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \

src/cbmc/bmc.cpp

@@ -131,12 +131,6 @@ safety_checkert::resultt bmct::execute(
       return safety_checkert::resultt::SAFE; // to indicate non-error
     }
 
-    if(!options.get_list_option("cover").empty())
-    {
-      return cover(goto_functions)?
-        safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
-    }
-
     // any properties to check at all?
     if(
       !options.get_bool_option("program-only") &&

src/cbmc/bmc.h

@@ -191,12 +191,7 @@ class bmct:public safety_checkert
   virtual resultt all_properties(const goto_functionst &goto_functions);
   virtual resultt stop_on_fail();
 
-  bool cover(const goto_functionst &goto_functions);
-
   friend class bmc_all_propertiest;
-  friend class bmc_covert;
-  template <template <class goalt> class covert>
-  friend class bmc_goal_covert;
 
 private:
   /// \brief Class-specific symbolic execution