Merge pull request #2439 from tautschnig/vs-pointer

Remove unused and inconsistent pointer_object_has_type

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -1164,26 +1164,6 @@ std::string expr2ct::convert_unary(
   return dest;
 }
 
-std::string expr2ct::convert_pointer_object_has_type(
-  const exprt &src,
-  unsigned precedence)
-{
-  if(src.operands().size()!=1)
-    return convert_norep(src, precedence);
-
-  unsigned p0;
-  std::string op0=convert_with_precedence(src.op0(), p0);
-
-  std::string dest="POINTER_OBJECT_HAS_TYPE";
-  dest+='(';
-  dest+=op0;
-  dest+=", ";
-  dest+=convert(static_cast<const typet &>(src.find("object_type")));
-  dest+=')';
-
-  return dest;
-}
-
 std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
 {
   if(src.operands().size() != 2)
@@ -3579,9 +3559,6 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()=="object_value")
     return convert_function(src, "OBJECT_VALUE", precedence=16);
 
-  else if(src.id()=="pointer_object_has_type")
-    return convert_pointer_object_has_type(src, precedence=16);
-
   else if(src.id()==ID_array_of)
     return convert_array_of(src, precedence=16);
 

src/ansi-c/expr2c_class.h

@@ -102,9 +102,6 @@ class expr2ct
   std::string convert_member(
     const member_exprt &src, unsigned precedence);
 
-  std::string convert_pointer_object_has_type(
-    const exprt &src, unsigned precedence);
-
   std::string convert_array_of(const exprt &src, unsigned precedence);
 
   std::string convert_trinary(

src/solvers/smt2/smt2_conv.cpp

@@ -1383,13 +1383,6 @@ void smt2_convt::convert_expr(const exprt &expr)
     out << ") (_ bv" << pointer_logic.get_invalid_object()
         << " " << config.bv_encoding.object_bits << "))";
   }
-  else if(expr.id()=="pointer_object_has_type")
-  {
-    assert(expr.operands().size()==1);
-
-    out << "false"; // TODO
-    SMT2_TODO("pointer_object_has_type not implemented");
-  }
   else if(expr.id()==ID_string_constant)
   {
     defined_expressionst::const_iterator it=defined_expressions.find(expr);

src/util/pointer_predicates.cpp

@@ -68,11 +68,6 @@ exprt dynamic_size(const namespacet &ns)
   return ns.lookup(CPROVER_PREFIX "malloc_size").symbol_expr();
 }
 
-exprt pointer_object_has_type(const exprt &pointer, const typet &type)
-{
-  return false_exprt();
-}
-
 exprt dynamic_object(const exprt &pointer)
 {
   exprt dynamic_expr(ID_dynamic_object, bool_typet());

src/util/pointer_predicates.h

@@ -24,8 +24,6 @@ exprt pointer_offset(const exprt &pointer);
 exprt pointer_object(const exprt &pointer);
 exprt malloc_object(const exprt &pointer, const namespacet &);
 exprt object_size(const exprt &pointer);
-exprt pointer_object_has_type(
-  const exprt &pointer, const typet &type, const namespacet &);
 exprt dynamic_object(const exprt &pointer);
 exprt good_pointer(const exprt &pointer);
 exprt good_pointer_def(const exprt &pointer, const namespacet &);