move nondet.h/.cpp and allocate_objects.h/.cpp

kroening · kroening · commit cab7f30447ba · 2021-10-21T18:26:43.000+01:00
This moves allocate_objects.h/.cpp to goto-programs, since it relates to
procedural code.

nondet.h/.cpp are moved to jbmc, which is where it is used.
diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile
@@ -48,6 +48,7 @@ SRC = assignments_from_json.cpp \
       lift_clinit_calls.cpp \
       load_method_by_regex.cpp \
       mz_zip_archive.cpp \
+      nondet.cpp \
       remove_exceptions.cpp \
       remove_instanceof.cpp \
       remove_java_new.cpp \
diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp
@@ -15,9 +15,9 @@ Author: Diffblue Ltd.
 #include "java_types.h"
 #include "java_utils.h"
 
+#include <goto-programs/allocate_objects.h>
 #include <goto-programs/class_identifier.h>
 
-#include <util/allocate_objects.h>
 #include <util/arith_tools.h>
 #include <util/array_element_from_pointer.h>
 #include <util/expr_initializer.h>
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/expr_initializer.h>
 #include <util/journalling_symbol_table.h>
-#include <util/nondet.h>
 #include <util/suffix.h>
 
 #include <goto-programs/adjust_float_expressions.h>
@@ -26,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_string_literals.h"
 #include "java_types.h"
 #include "java_utils.h"
+#include "nondet.h"
 
 #include <cstring>
 
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/array_element_from_pointer.h>
 #include <util/expr_initializer.h>
 #include <util/message.h>
-#include <util/nondet.h>
 #include <util/nondet_bool.h>
 #include <util/prefix.h>
 
diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h
@@ -71,8 +71,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
 #define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
 
-#include <util/allocate_objects.h>
-#include <util/nondet.h>
+#include "nondet.h"
+
+#include <goto-programs/allocate_objects.h>
+
 #include <util/std_code.h>
 
 class message_handlert;
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -16,9 +16,9 @@ Date:   April 2017
 ///   java standard library. In particular methods from java.lang.String,
 ///   java.lang.StringBuilder, java.lang.StringBuffer.
 
+#include <goto-programs/allocate_objects.h>
 #include <goto-programs/class_identifier.h>
 
-#include <util/allocate_objects.h>
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
diff --git a/jbmc/src/java_bytecode/nondet.cpp b/jbmc/src/java_bytecode/nondet.cpp
@@ -8,8 +8,9 @@ Author: Diffblue Ltd.
 
 #include "nondet.h"
 
-#include "allocate_objects.h"
-#include "arith_tools.h"
+#include <goto-programs/allocate_objects.h>
+
+#include <util/arith_tools.h>
 
 symbol_exprt generate_nondet_int(
   const exprt &min_value_expr,
diff --git a/jbmc/src/java_bytecode/nondet.h b/jbmc/src/java_bytecode/nondet.h
@@ -9,7 +9,7 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_BYTECODE_NONDET_H
 #define CPROVER_JAVA_BYTECODE_NONDET_H
 
-#include "std_code.h"
+#include <util/std_code.h>
 
 class allocate_objectst;
 class symbol_table_baset;
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -13,14 +13,14 @@ Author: Diffblue Ltd.
 
 #include <ansi-c/c_object_factory_parameters.h>
 
-#include <util/allocate_objects.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/nondet_bool.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
 
+#include <goto-programs/allocate_objects.h>
 #include <goto-programs/goto_functions.h>
 
 /// Creates a nondet for expr, including calling itself recursively to make
diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h
@@ -14,7 +14,8 @@ Author: Diffblue Ltd.
 
 #include <set>
 
-#include <util/allocate_objects.h>
+#include <goto-programs/allocate_objects.h>
+
 #include <util/symbol_table.h>
 
 struct c_object_factory_parameterst;
diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp
@@ -8,7 +8,6 @@ Author: Diffblue Ltd.
 
 #include "function_call_harness_generator.h"
 
-#include <util/allocate_objects.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
@@ -18,6 +17,7 @@ Author: Diffblue Ltd.
 #include <util/string_utils.h>
 #include <util/ui_message.h>
 
+#include <goto-programs/allocate_objects.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_model.h>
 
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
@@ -1,4 +1,5 @@
-SRC = add_malloc_may_fail_variable_initializations.cpp \
+SRC = allocate_objects.cpp \
+      add_malloc_may_fail_variable_initializations.cpp \
       adjust_float_expressions.cpp \
       builtin_functions.cpp \
       class_hierarchy.cpp \
diff --git a/src/goto-programs/allocate_objects.cpp b/src/goto-programs/allocate_objects.cpp
@@ -8,11 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "allocate_objects.h"
 
-#include "c_types.h"
-#include "fresh_symbol.h"
-#include "pointer_expr.h"
-#include "pointer_offset_size.h"
-#include "symbol.h"
+#include <util/c_types.h>
+#include <util/fresh_symbol.h>
+#include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
+#include <util/symbol.h>
 
 /// Allocates a new object, either by creating a local variable with automatic
 /// lifetime, a global variable with static lifetime, or by dynamically
diff --git a/src/goto-programs/allocate_objects.h b/src/goto-programs/allocate_objects.h
@@ -9,9 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H
 #define CPROVER_UTIL_ALLOCATE_OBJECTS_H
 
-#include "goto_instruction_code.h"
-#include "namespace.h"
-#include "source_location.h"
+#include <util/goto_instruction_code.h>
+#include <util/namespace.h>
+#include <util/source_location.h>
 
 /// Selects the kind of objects allocated
 enum class lifetimet
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
@@ -16,14 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <vector>
 #include <unordered_set>
 
-#include <util/allocate_objects.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/replace_expr.h>
 #include <util/std_code.h>
 
-#include "goto_program.h"
+#include "allocate_objects.h"
 #include "destructor_tree.h"
+#include "goto_program.h"
 
 class side_effect_expr_overflowt;
 
diff --git a/src/memory-analyzer/analyze_symbol.h b/src/memory-analyzer/analyze_symbol.h
@@ -20,12 +20,13 @@ Author: Malte Mues <mail.mues@gmail.com>
 
 #include <ansi-c/expr2c_class.h>
 
-#include <util/allocate_objects.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
+#include <goto-programs/allocate_objects.h>
+
 class gdb_apit;
 class exprt;
 class source_locationt;
diff --git a/src/util/Makefile b/src/util/Makefile
@@ -1,5 +1,4 @@
-SRC = allocate_objects.cpp \
-      arith_tools.cpp \
+SRC = arith_tools.cpp \
       array_element_from_pointer.cpp \
       array_name.cpp \
       base_type.cpp \
@@ -54,7 +53,6 @@ SRC = allocate_objects.cpp \
       message.cpp \
       mp_arith.cpp \
       namespace.cpp \
-      nondet.cpp \
       object_factory_parameters.cpp \
       options.cpp \
       parse_options.cpp \
diff --git a/unit/Makefile b/unit/Makefile
@@ -59,6 +59,7 @@ SRC += analyses/ai/ai.cpp \
        goto-checker/report_util/is_property_less_than.cpp \
        goto-instrument/cover_instrument.cpp \
        goto-instrument/cover/cover_only.cpp \
+       goto-programs/allocate_objects.cpp \
        goto-programs/goto_program_assume.cpp \
        goto-programs/goto_program_dead.cpp \
        goto-programs/goto_program_declaration.cpp \
@@ -118,7 +119,6 @@ SRC += analyses/ai/ai.cpp \
        solvers/strings/string_refinement/string_refinement.cpp \
        solvers/strings/string_refinement/substitute_array_list.cpp \
        solvers/strings/string_refinement/union_find_replace.cpp \
-       util/allocate_objects.cpp \
        util/cmdline.cpp \
        util/dense_integer_map.cpp \
        util/edit_distance.cpp \
diff --git a/unit/goto-programs/allocate_objects.cpp b/unit/goto-programs/allocate_objects.cpp
@@ -6,16 +6,16 @@ Author: Diffblue Ltd
 
 \*******************************************************************/
 
-#include <util/allocate_objects.h>
+#include <goto-programs/allocate_objects.h>
+
 #include <util/c_types.h>
-#include <util/source_location.h>
 #include <util/symbol_table.h>
 
 #include <testing-utils/use_catch.h>
 
 TEST_CASE(
   "Tests the absence of a bug that crashed allocate_objects",
-  "[core][util][allocate_objects]")
+  "[core][goto-programs][allocate_objects]")
 {
   symbol_tablet symtab{};
   // Because __a_temp will return a const reference to temporary
