Merge pull request #2943 from diffblue/cleanout-symex-dereference-failure

remove dereference checks during symex

Author: Daniel Kroening

src/goto-symex/symex_dereference_state.cpp

@@ -13,13 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 
-void symex_dereference_statet::dereference_failure(
-  const std::string &,
-  const std::string &,
-  const guardt &)
-{
-}
-
 bool symex_dereference_statet::has_failed_symbol(
   const exprt &expr,
   const symbolt *&symbol)

src/goto-symex/symex_dereference_state.h

@@ -32,11 +32,6 @@ class symex_dereference_statet:
   goto_symext &goto_symex;
   goto_symext::statet &state;
 
-  virtual void dereference_failure(
-    const std::string &property,
-    const std::string &msg,
-    const guardt &guard);
-
   virtual void get_value_set(
     const exprt &expr,
     value_setst::valuest &value_set);

src/pointer-analysis/dereference_callback.h

@@ -27,11 +27,6 @@ class dereference_callbackt
 public:
   virtual ~dereference_callbackt();
 
-  virtual void dereference_failure(
-    const std::string &property,
-    const std::string &msg,
-    const guardt &guard)=0;
-
   virtual void get_value_set(
     const exprt &expr,
     value_setst::valuest &value_set)=0;