From 0e9aa9068e45c46d8e4ed83eb3cde58ab88c32fc Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Jun 2018 12:38:36 +0100
Subject: [PATCH] Remove unused and inconsistent pointer_object_has_type

Its definition was incomplete and necessarily unused as it didn't match its
declaration.
---
 src/ansi-c/expr2c.cpp           | 23 -----------------------
 src/ansi-c/expr2c_class.h       |  3 ---
 src/solvers/smt2/smt2_conv.cpp  |  7 -------
 src/util/pointer_predicates.cpp |  5 -----
 src/util/pointer_predicates.h   |  2 --
 5 files changed, 40 deletions(-)

diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index be545dad05f..d1bf4d069e5 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/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);
 
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
index 2e33e21ec9f..a2424b8e5e3 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/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(
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 0cd206a36df..c1b14961d76 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/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);
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
index 966ebdae021..855160520e5 100644
--- a/src/util/pointer_predicates.cpp
+++ b/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());
diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h
index ca149cfbc83..8739cd5026e 100644
--- a/src/util/pointer_predicates.h
+++ b/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 &);