Create is_invalid_pointer_exprt class

Author: Owen

src/util/pointer_predicates.cpp

@@ -141,7 +141,7 @@ exprt null_pointer(const exprt &pointer)
 
 exprt is_invalid_pointer(const exprt &pointer)
 {
-  return unary_exprt(ID_is_invalid_pointer, pointer, bool_typet());
+  return is_invalid_pointer_exprt{pointer};
 }
 
 exprt dynamic_object_lower_bound(

src/util/pointer_predicates.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_POINTER_PREDICATES_H
 #define CPROVER_UTIL_POINTER_PREDICATES_H
 
+#include "std_expr.h"
 #define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
 
 class exprt;
@@ -47,4 +48,13 @@ exprt object_upper_bound(
   const exprt &pointer,
   const exprt &access_size);
 
+class is_invalid_pointer_exprt : public unary_predicate_exprt
+{
+public:
+  explicit is_invalid_pointer_exprt(exprt pointer)
+    : unary_predicate_exprt{ID_is_invalid_pointer, std::move(pointer)}
+  {
+  }
+};
+
 #endif // CPROVER_UTIL_POINTER_PREDICATES_H