Merge pull request #5894 from diffblue/pointer_expr_h_fixup

move null_pointer_exprt to pointer_expr.h

Author: kroening

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_types.h"
 #include "remove_exceptions.h"
 
-#include <util/std_types.h>
-#include <util/cprover_prefix.h>
 #include <util/c_types.h>
+#include <util/cprover_prefix.h>
+#include <util/pointer_expr.h>
+#include <util/std_types.h>
 
 void java_internal_additions(symbol_table_baset &dest)
 {

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -22,8 +22,9 @@ Date:   December 2016
 #include <algorithm>
 
 #include <util/c_types.h>
-#include <util/std_expr.h>
+#include <util/pointer_expr.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/remove_skip.h>

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

@@ -10,7 +10,9 @@ Author: Diffblue Ltd.
 #include <java-testing-utils/load_java_class.h>
 #include <testing-utils/use_catch.h>
 
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
+
 #include <goto-programs/remove_virtual_functions.h>
 
 /// Try to resolve a classid comparison `expr`, assuming that any accessed

scripts/expected_doxygen_warnings.txt

@@ -92,7 +92,7 @@ warning: Included by graph for 'invariant.h' not generated, too many nodes (187)
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (101), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (106), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -19,6 +19,7 @@ Author: Diffblue Ltd.
 #include <util/fresh_symbol.h>
 #include <util/namespace.h>
 #include <util/nondet_bool.h>
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>

src/util/arith_tools.cpp

@@ -11,8 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "invariant.h"
-#include "std_types.h"
+#include "pointer_expr.h"
 #include "std_expr.h"
+#include "std_types.h"
 
 #include <algorithm>
 

src/util/pointer_expr.h

@@ -326,4 +326,14 @@ inline dereference_exprt &to_dereference_expr(exprt &expr)
   return ret;
 }
 
+/// \brief The null pointer constant
+class null_pointer_exprt : public constant_exprt
+{
+public:
+  explicit null_pointer_exprt(pointer_typet type)
+    : constant_exprt(ID_NULL, std::move(type))
+  {
+  }
+};
+
 #endif // CPROVER_UTIL_POINTER_EXPR_H

src/util/pointer_predicates.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_types.h"
 #include "cprover_prefix.h"
 #include "namespace.h"
+#include "pointer_expr.h"
 #include "pointer_offset_size.h"
 #include "std_expr.h"
 #include "symbol.h"

src/util/std_expr.h

@@ -2746,17 +2746,6 @@ inline bool can_cast_expr<nil_exprt>(const exprt &base)
   return base.id() == ID_nil;
 }
 
-/// \brief The null pointer constant
-class null_pointer_exprt:public constant_exprt
-{
-public:
-  explicit null_pointer_exprt(pointer_typet type)
-    : constant_exprt(ID_NULL, std::move(type))
-  {
-  }
-};
-
-
 /// \brief An expression denoting infinity
 class infinity_exprt : public nullary_exprt
 {

unit/interpreter/interpreter.cpp

@@ -10,9 +10,11 @@ Author: Diffblue Ltd.
 
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/interpreter_class.h>
+
 #include <util/message.h>
 #include <util/mp_arith.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 
 typedef interpretert::mp_vectort mp_vectort;