Merge pull request #1823 from diffblue/cleanup

Clean out various bits of legacy code

Author: kroening

src/goto-programs/goto_convert.cpp

@@ -515,10 +515,6 @@ void goto_convertt::convert(
     convert_atomic_begin(code, dest);
   else if(statement==ID_atomic_end)
     convert_atomic_end(code, dest);
-  else if(statement==ID_bp_enforce)
-    convert_bp_enforce(code, dest);
-  else if(statement==ID_bp_abortif)
-    convert_bp_abortif(code, dest);
   else if(statement==ID_cpp_delete ||
           statement=="cpp_delete[]")
     convert_cpp_delete(code, dest);
@@ -1604,88 +1600,6 @@ void goto_convertt::convert_atomic_end(
   copy(code, ATOMIC_END, dest);
 }
 
-void goto_convertt::convert_bp_enforce(
-  const codet &code,
-  goto_programt &dest)
-{
-  if(code.operands().size()!=2)
-  {
-    error().source_location=code.find_source_location();
-    error() << "bp_enfroce expects two arguments" << eom;
-    throw 0;
-  }
-
-  // do an assume
-  exprt op=code.op0();
-
-  clean_expr(op, dest);
-
-  goto_programt::targett t=dest.add_instruction(ASSUME);
-  t->guard=op;
-  t->source_location=code.source_location();
-
-  // change the assignments
-
-  goto_programt tmp;
-  convert(to_code(code.op1()), tmp);
-
-  if(!op.is_true())
-  {
-    exprt constraint(op);
-    make_next_state(constraint);
-
-    Forall_goto_program_instructions(it, tmp)
-    {
-      if(it->is_assign())
-      {
-        assert(it->code.get(ID_statement)==ID_assign);
-
-        // add constrain
-        codet constrain(ID_bp_constrain);
-        constrain.reserve_operands(2);
-        constrain.move_to_operands(it->code);
-        constrain.copy_to_operands(constraint);
-        it->code.swap(constrain);
-
-        it->type=OTHER;
-      }
-      else if(it->is_other() &&
-              it->code.get(ID_statement)==ID_bp_constrain)
-      {
-        // add to constraint
-        assert(it->code.operands().size()==2);
-        it->code.op1()=
-          and_exprt(it->code.op1(), constraint);
-      }
-    }
-  }
-
-  dest.destructive_append(tmp);
-}
-
-void goto_convertt::convert_bp_abortif(
-  const codet &code,
-  goto_programt &dest)
-{
-  if(code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "bp_abortif expects one argument" << eom;
-    throw 0;
-  }
-
-  // do an assert
-  exprt op=code.op0();
-
-  clean_expr(op, dest);
-
-  op.make_not();
-
-  goto_programt::targett t=dest.add_instruction(ASSERT);
-  t->guard.swap(op);
-  t->source_location=code.source_location();
-}
-
 void goto_convertt::convert_ifthenelse(
   const code_ifthenelset &code,
   goto_programt &dest)

src/goto-programs/goto_convert_class.h

@@ -234,8 +234,6 @@ class goto_convertt:public messaget
   void convert_end_thread(const codet &code, goto_programt &dest);
   void convert_atomic_begin(const codet &code, goto_programt &dest);
   void convert_atomic_end(const codet &code, goto_programt &dest);
-  void convert_bp_enforce(const codet &code, goto_programt &dest);
-  void convert_bp_abortif(const codet &code, goto_programt &dest);
   void convert_msc_try_finally(const codet &code, goto_programt &dest);
   void convert_msc_try_except(const codet &code, goto_programt &dest);
   void convert_msc_leave(const codet &code, goto_programt &dest);

src/util/decision_procedure.cpp

@@ -11,10 +11,4 @@ Author: Daniel Kroening, [email protected]
 
 #include "decision_procedure.h"
 
-#include <cassert>
 
-bool decision_proceduret::in_core(const exprt &expr)
-{
-  UNREACHABLE;
-  return true;
-}

src/util/decision_procedure.h

@@ -52,9 +52,6 @@ class decision_proceduret:public messaget
     return dec_solve();
   }
 
-  // old-style, will go away
-  virtual bool in_core(const exprt &expr);
-
   // return a textual description of the decision procedure
   virtual std::string decision_procedure_text() const=0;
 

src/util/expr_util.cpp

@@ -17,15 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include "namespace.h"
 #include "arith_tools.h"
 
-void make_next_state(exprt &expr)
-{
-  Forall_operands(it, expr)
-    make_next_state(*it);
-
-  if(expr.id()==ID_symbol)
-    expr.id(ID_next_symbol);
-}
-
 exprt make_binary(const exprt &expr)
 {
   const exprt::operandst &operands=expr.operands();

src/util/expr_util.h

@@ -28,11 +28,6 @@ class symbolt;
 class typet;
 class namespacet;
 
-/// \deprecated This function will eventually be removed. Use functions
-/// from \ref util/std_expr.h instead.
-
-void make_next_state(exprt &);
-
 /// splits an expression with >=3 operands into nested binary expressions
 exprt make_binary(const exprt &);
 

src/util/format_constant.cpp

@@ -25,7 +25,7 @@ std::string format_constantt::operator()(const exprt &expr)
        expr.type().id()==ID_signedbv)
     {
       mp_integer i;
-      if(to_integer(expr, i))
+      if(to_integer(to_constant_expr(expr), i))
         return "(number conversion failed)";
 
       return integer2string(i);

src/util/std_expr.h

@@ -3837,11 +3837,6 @@ inline void validate_expr(const array_update_exprt &value)
 class member_exprt:public unary_exprt
 {
 public:
-  // deprecated, and will go away -- use either of the two below
-  explicit member_exprt(const typet &_type):unary_exprt(ID_member, _type)
-  {
-  }
-
   member_exprt(
     const exprt &op,
     const irep_idt &component_name,

src/util/xml_expr.cpp

@@ -159,7 +159,8 @@ xmlt xml(
       std::size_t width=to_bitvector_type(type).get_width();
 
       result.name="integer";
-      result.set_attribute("binary", expr.get_string(ID_value));
+      result.set_attribute("binary",
+        id2string(to_constant_expr(expr).get_value()));
       result.set_attribute("width", width);
 
       const typet &underlying_type=
@@ -182,7 +183,7 @@ xmlt xml(
         result.set_attribute("c_type", sig+"long long int");
 
       mp_integer i;
-      if(!to_integer(expr, i))
+      if(!to_integer(to_constant_expr(expr), i))
         result.data=integer2string(i);
     }
     else if(type.id()==ID_c_enum)
@@ -193,7 +194,7 @@ xmlt xml(
       result.set_attribute("c_type", "enum");
 
       mp_integer i;
-      if(!to_integer(expr, i))
+      if(!to_integer(to_constant_expr(expr), i))
         result.data=integer2string(i);
     }
     else if(type.id()==ID_c_enum_tag)