Merge pull request #5763 from diffblue/pointer_expr_h

move pointer-related expression classes into separate header file

Author: kroening

jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp

@@ -12,9 +12,12 @@ Author: Diffblue Ltd.
 #include "create_array_with_type_intrinsic.h"
 
 #include <goto-programs/class_identifier.h>
+
 #include <java_bytecode/java_types.h>
+
 #include <util/fresh_symbol.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/symbol_table_base.h>
 
 /// Returns the symbol name for `org.cprover.CProver.createArrayWithType`

jbmc/src/java_bytecode/java_pointer_casts.cpp

@@ -11,9 +11,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_pointer_casts.h"
 
+#include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
-#include <util/namespace.h>
 
 #include "java_types.h"
 

jbmc/src/java_bytecode/java_trace_validation.cpp

@@ -11,9 +11,11 @@ Author: Jeannie Moulton
 #include <algorithm>
 
 #include <goto-programs/goto_trace.h>
+
 #include <util/byte_operators.h>
 #include <util/expr.h>
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 

jbmc/src/java_bytecode/java_utils.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/nodiscard.h>
 #include <util/optional.h>
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 

jbmc/unit/java-testing-utils/require_goto_statements.cpp

@@ -10,14 +10,18 @@ Author: Diffblue Ltd.
 
 #include <testing-utils/use_catch.h>
 
-#include <algorithm>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
+
 #include <java_bytecode/java_types.h>
+
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
 #include <util/suffix.h>
 
+#include <algorithm>
+
 /// Expand value of a function to include all child codets
 /// \param function_value: The value of the function (e.g. got by looking up
 ///  the function in the symbol table and getting the value)

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -7,11 +7,15 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include <goto-programs/goto_trace.h>
+
 #include <java_bytecode/java_trace_validation.h>
 #include <java_bytecode/java_types.h>
+
 #include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
+
 #include <util/byte_operators.h>
+#include <util/pointer_expr.h>
 
 TEST_CASE("java trace validation", "[core][java_trace_validation]")
 {

jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -23,6 +23,7 @@ Author: Chris Smowton, [email protected]
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/options.h>
+#include <util/pointer_expr.h>
 
 /// An example customised value_sett. It makes a series of small changes
 /// to the underlying value_sett logic, which can then be verified by the

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -11,7 +11,6 @@ Author: Jesse Sigal, [email protected]
 
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_types.h>
-#include <numeric>
 
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
@@ -22,8 +21,11 @@ Author: Jesse Sigal, [email protected]
 #include <util/config.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 
+#include <numeric>
+
 /// \class Types used throughout the test. Currently it is impossible to
 /// statically initialize this value, there is a PR to allow this
 /// diffblue/cbmc/pull/1213

scripts/expected_doxygen_warnings.txt

@@ -83,19 +83,20 @@ warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many node
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'c_types.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'expr_util.h' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 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 (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'namespace.h' not generated, too many nodes (112), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'namespace.h' not generated, too many nodes (113), 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 '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 (76), 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.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (249), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (248), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/ai_domain.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ai_domain.h"
 
+#include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 
 jsont ai_domain_baset::output_json(const ai_baset &ai, const namespacet &ns)