Merge pull request #8253 from diffblue/move-goto-convert

Move goto_convert files

Author: kroening

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -16,10 +16,11 @@ Author: Diffblue Ltd.
 #include <util/symbol_table_base.h>
 #include <util/unicode.h>
 
-#include <goto-programs/allocate_objects.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_instruction_code.h>
 
+#include <ansi-c/allocate_objects.h>
+
 #include "ci_lazy_methods_needed.h"
 #include "code_with_references.h"
 #include "java_static_initializers.h"

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -11,10 +11,11 @@ Author: Reuben Thomas, [email protected]
 
 #include "convert_java_nondet.h"
 
-#include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
+#include <ansi-c/goto-conversion/goto_convert.h>
+
 #include "java_object_factory.h" // gen_nondet_init
 #include "java_object_factory_parameters.h"
 #include "java_utils.h"

jbmc/src/java_bytecode/java_object_factory.h

@@ -71,11 +71,11 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
 #define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
 
-#include "nondet.h"
+#include <util/std_code.h>
 
-#include <goto-programs/allocate_objects.h>
+#include <ansi-c/allocate_objects.h>
 
-#include <util/std_code.h>
+#include "nondet.h"
 
 class message_handlert;
 class select_pointer_typet;

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -29,9 +29,10 @@ Date:   April 2017
 #include <util/string_expr.h>
 #include <util/symbol_table_base.h>
 
-#include <goto-programs/allocate_objects.h>
 #include <goto-programs/class_identifier.h>
 
+#include <ansi-c/allocate_objects.h>
+
 #include "java_types.h"
 #include "java_utils.h"
 

jbmc/src/java_bytecode/lazy_goto_functions_map.h

@@ -6,15 +6,16 @@
 #ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
 #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
 
-#include <unordered_set>
+#include <util/journalling_symbol_table.h>
+#include <util/message.h>
+#include <util/symbol_table_builder.h>
 
-#include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_functions.h>
 
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <langapi/language_file.h>
-#include <util/journalling_symbol_table.h>
-#include <util/message.h>
-#include <util/symbol_table_builder.h>
+
+#include <unordered_set>
 
 /// Provides a wrapper for a map of lazily loaded goto_functiont.
 /// This incrementally builds a goto-functions object, while permitting

jbmc/src/java_bytecode/nondet.cpp

@@ -8,10 +8,10 @@ Author: Diffblue Ltd.
 
 #include "nondet.h"
 
-#include <goto-programs/allocate_objects.h>
-
 #include <util/arith_tools.h>
 
+#include <ansi-c/allocate_objects.h>
+
 symbol_exprt generate_nondet_int(
   const exprt &min_value_expr,
   const exprt &max_value_expr,

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -19,9 +19,10 @@ Author: Peter Schrammel
 #include <util/std_code.h>
 
 #include <goto-programs/class_identifier.h>
-#include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_model.h>
 
+#include <ansi-c/goto-conversion/goto_convert.h>
+
 #include "java_types.h"
 #include "java_utils.h"
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -20,7 +20,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_check.h>
-#include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/remove_returns.h>
@@ -33,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_symbol_table.h>
 
 #include <ansi-c/ansi_c_language.h>
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/all_properties_verifier_with_fault_localization.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>

jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt

@@ -1,3 +1,4 @@
+ansi-c
 testing-utils
 java-testing-utils
 analyses

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

@@ -8,13 +8,14 @@ Author: Diffblue Limited.
 \*******************************************************************/
 
 #include <java-testing-utils/load_java_class.h>
-#include <testing-utils/message.h>
-#include <testing-utils/use_catch.h>
 
-#include <analyses/local_safe_pointers.h>
-#include <goto-programs/goto_convert_functions.h>
 #include <util/expr_iterator.h>
 
+#include <analyses/local_safe_pointers.h>
+#include <ansi-c/goto-conversion/goto_convert_functions.h>
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
+
 // We're expecting a call "something->field . B.virtualmethod()":
 static bool is_expected_virtualmethod_call(
   const goto_programt::instructiont &instruction)