Remove unused code from goto_program_dereference

A lot of code in goto_program_dereference was deprecated, commented or
documented as unused. This commit remove these parts of the code.

Author: romainbrenguier

src/pointer-analysis/goto_program_dereference.cpp

@@ -44,56 +44,6 @@ goto_program_dereferencet::get_or_create_failed_symbol(const exprt &expr)
   return nullptr;
 }
 
-/// \deprecated
-bool goto_program_dereferencet::is_valid_object(
-  const irep_idt &identifier)
-{
-  const symbolt &symbol=ns.lookup(identifier);
-
-  if(symbol.type.id()==ID_code)
-    return true;
-
-  if(symbol.is_static_lifetime)
-    return true; // global/static
-
-  #if 0
-  return valid_local_variables->find(symbol.name)!=
-     valid_local_variables->end(); // valid local
-  #else
-  return true;
-  #endif
-}
-
-/// \deprecated
-void goto_program_dereferencet::dereference_failure(
-  const std::string &property,
-  const std::string &msg,
-  const guardt &guard)
-{
-  exprt guard_expr=guard.as_expr();
-
-  if(assertions.insert(guard_expr).second)
-  {
-    guard_expr = boolean_negate(guard_expr);
-
-    // first try simplifier on it
-    if(options.get_bool_option("simplify"))
-      simplify(guard_expr, ns);
-
-    if(!guard_expr.is_true())
-    {
-      goto_program_instruction_typet type=
-        options.get_bool_option("assert-to-assume")?ASSUME:ASSERT;
-
-      goto_programt::targett t=new_code.add_instruction(type);
-      t->guard.swap(guard_expr);
-      t->source_location=dereference_location;
-      t->source_location.set_property_class(property);
-      t->source_location.set_comment("dereference failure: "+msg);
-    }
-  }
-}
-
 /// Turn subexpression of `expr` of the form `&*p` into p
 /// and use `dereference` on subexpressions of the form `*p`
 /// \param expr: expression in which to remove dereferences
@@ -166,8 +116,6 @@ void goto_program_dereferencet::dereference_rec(exprt &expr)
     if(expr.operands().size()!=1)
       throw "dereference expects one operand";
 
-    dereference_location=expr.find_source_location();
-
     exprt tmp = dereference.dereference(expr.op0());
 
     expr.swap(tmp);
@@ -181,8 +129,6 @@ void goto_program_dereferencet::dereference_rec(exprt &expr)
 
     if(expr.op0().type().id()==ID_pointer)
     {
-      dereference_location=expr.find_source_location();
-
       exprt tmp1(ID_plus, expr.op0().type());
       tmp1.operands().swap(expr.operands());
 
@@ -231,8 +177,6 @@ void goto_program_dereferencet::dereference_program(
       it++)
   {
     new_code.clear();
-    assertions.clear();
-
     dereference_instruction(it, checks_only);
 
     // insert new instructions
@@ -265,9 +209,6 @@ void goto_program_dereferencet::dereference_instruction(
   bool checks_only)
 {
   current_target=target;
-  #if 0
-  valid_local_variables=&target->local_variables;
-  #endif
   goto_programt::instructiont &i=*target;
 
   if(i.has_condition())
@@ -329,45 +270,9 @@ void goto_program_dereferencet::dereference_expression(
 {
   current_function = function_id;
   current_target=target;
-  #if 0
-  valid_local_variables=&target->local_variables;
-  #endif
-
   dereference_expr(expr, false);
 }
 
-/// Throw an exception in case removing dereferences from the program would
-/// throw an exception.
-void goto_program_dereferencet::pointer_checks(
-  goto_programt &goto_program)
-{
-  dereference_program(goto_program, true);
-}
-
-/// Throw an exception in case removing dereferences from the program would
-/// throw an exception.
-void goto_program_dereferencet::pointer_checks(
-  goto_functionst &goto_functions)
-{
-  dereference_program(goto_functions, true);
-}
-
-/// \deprecated
-void remove_pointers(
-  goto_programt &goto_program,
-  symbol_tablet &symbol_table,
-  value_setst &value_sets)
-{
-  namespacet ns(symbol_table);
-
-  optionst options;
-
-  goto_program_dereferencet
-    goto_program_dereference(ns, symbol_table, options, value_sets);
-
-  goto_program_dereference.dereference_program(goto_program);
-}
-
 /// Remove dereferences in all expressions contained in the program
 /// `goto_model`. `value_sets` is used to determine to what objects the pointers
 /// may be pointing to.
@@ -387,32 +292,6 @@ void remove_pointers(
     goto_program_dereference.dereference_program(it->second.body);
 }
 
-/// \deprecated
-void pointer_checks(
-  goto_programt &goto_program,
-  symbol_tablet &symbol_table,
-  const optionst &options,
-  value_setst &value_sets)
-{
-  namespacet ns(symbol_table);
-  goto_program_dereferencet
-    goto_program_dereference(ns, symbol_table, options, value_sets);
-  goto_program_dereference.pointer_checks(goto_program);
-}
-
-/// \deprecated
-void pointer_checks(
-  goto_functionst &goto_functions,
-  symbol_tablet &symbol_table,
-  const optionst &options,
-  value_setst &value_sets)
-{
-  namespacet ns(symbol_table);
-  goto_program_dereferencet
-    goto_program_dereference(ns, symbol_table, options, value_sets);
-  goto_program_dereference.pointer_checks(goto_functions);
-}
-
 /// Remove dereferences in `expr` using `value_sets` to determine to what
 /// objects the pointers may be pointing to.
 void dereference(

src/pointer-analysis/goto_program_dereference.h

@@ -19,8 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include "value_sets.h"
 #include "value_set_dereference.h"
 
-class guardt;
-
 /// Wrapper for functions removing dereferences in expressions contained in
 /// a goto program.
 class goto_program_dereferencet:protected dereference_callbackt
@@ -50,9 +48,6 @@ class goto_program_dereferencet:protected dereference_callbackt
     goto_functionst &goto_functions,
     bool checks_only=false);
 
-  void pointer_checks(goto_programt &goto_program);
-  void pointer_checks(goto_functionst &goto_functions);
-
   void dereference_expression(
     const irep_idt &function_id,
     goto_programt::const_targett target,
@@ -68,17 +63,8 @@ class goto_program_dereferencet:protected dereference_callbackt
   value_setst &value_sets;
   value_set_dereferencet dereference;
 
-  DEPRECATED("Unused")
-  virtual bool is_valid_object(const irep_idt &identifier);
-
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 
-  DEPRECATED("Unused")
-  virtual void dereference_failure(
-    const std::string &property,
-    const std::string &msg,
-    const guardt &guard);
-
   void
   get_value_set(const exprt &expr, value_setst::valuest &dest) const override;
 
@@ -90,19 +76,8 @@ class goto_program_dereferencet:protected dereference_callbackt
   void dereference_rec(exprt &expr);
   void dereference_expr(exprt &expr, const bool checks_only);
 
-#if 0
-  const std::set<irep_idt> *valid_local_variables;
-#endif
   irep_idt current_function;
   goto_programt::const_targett current_target;
-
-  /// Unused
-  source_locationt dereference_location;
-
-  /// Unused
-  std::set<exprt> assertions;
-
-  /// Unused
   goto_programt new_code;
 };
 
@@ -117,24 +92,4 @@ void remove_pointers(
   goto_modelt &,
   value_setst &);
 
-DEPRECATED("Unused")
-void remove_pointers(
-  goto_functionst &,
-  symbol_tablet &,
-  value_setst &);
-
-DEPRECATED("Unused")
-void pointer_checks(
-  goto_programt &,
-  symbol_tablet &,
-  const optionst &,
-  value_setst &);
-
-DEPRECATED("Unused")
-void pointer_checks(
-  goto_functionst &,
-  symbol_tablet &,
-  const optionst &,
-  value_setst &);
-
 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H