Remove ID_float_debug1 and ID_float_debug2 expressions

Author: danpoe

src/ansi-c/c_typecheck_expr.cpp

@@ -2724,26 +2724,6 @@ exprt c_typecheck_baset::do_special_functions(
 
     return tmp;
   }
-  else if(identifier==CPROVER_PREFIX "float_debug1" ||
-          identifier==CPROVER_PREFIX "float_debug2")
-  {
-    if(expr.arguments().size()!=2)
-    {
-      err_location(f_op);
-      error() << "float_debug expects two operands" << eom;
-      throw 0;
-    }
-
-    const irep_idt &id=
-      identifier==CPROVER_PREFIX "float_debug1"?
-      "float_debug1":"float_debug2";
-
-    exprt float_debug_expr(id, expr.type());
-    float_debug_expr.operands()=expr.arguments();
-    float_debug_expr.add_source_location()=source_location;
-
-    return float_debug_expr;
-  }
   else if(identifier=="__sync_fetch_and_add" ||
           identifier=="__sync_fetch_and_sub" ||
           identifier=="__sync_fetch_and_or" ||

src/solvers/flattening/boolbv.cpp

@@ -303,18 +303,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_not(to_not_expr(expr));
   else if(expr.id()==ID_power)
      return convert_power(to_binary_expr(expr));
-  else if(expr.id()==ID_float_debug1 ||
-          expr.id()==ID_float_debug2)
-  {
-    DATA_INVARIANT(expr.operands().size() == 2, "");
-    bvt bv0=convert_bitvector(expr.op0());
-    bvt bv1=convert_bitvector(expr.op1());
-    float_utilst float_utils(prop, to_floatbv_type(expr.type()));
-    bvt bv=expr.id()==ID_float_debug1?
-      float_utils.debug1(bv0, bv1):
-      float_utils.debug2(bv0, bv1);
-    return bv;
-  }
   else if(expr.id() == ID_popcount)
     return convert_bv(lower_popcount(to_popcount_expr(expr), ns));
 

src/util/irep_ids.def

@@ -514,8 +514,6 @@ IREP_ID_ONE(ptr_object)
 IREP_ID_TWO(C_c_sizeof_type, #c_sizeof_type)
 IREP_ID_ONE(array_update)
 IREP_ID_ONE(update)
-IREP_ID_ONE(float_debug1)
-IREP_ID_ONE(float_debug2)
 IREP_ID_ONE(static_assert)
 IREP_ID_ONE(gcc_attribute_mode)
 IREP_ID_TWO(built_in, <built-in>)