Merge pull request #6386 from diffblue/goto_instruction_code

kroening · web-flow · commit a80fe1fdcadf · 2021-10-08T19:00:47.000+01:00
Separate header file for goto-instruction codet types
diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.h b/jbmc/src/java_bytecode/character_refine_preprocess.h
@@ -20,8 +20,9 @@ Date:   March 2017
 #ifndef CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
 #define CPROVER_JAVA_BYTECODE_CHARACTER_REFINE_PREPROCESS_H
 
-#include <util/std_code.h>
+#include <util/goto_instruction_code.h>
 #include <util/mp_arith.h>
+#include <util/std_code.h>
 
 #include <unordered_map>
 
diff --git a/jbmc/src/java_bytecode/code_with_references.cpp b/jbmc/src/java_bytecode/code_with_references.cpp
@@ -8,7 +8,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include "code_with_references.h"
 #include "java_types.h"
+
 #include <util/arith_tools.h>
+#include <util/goto_instruction_code.h>
 
 codet allocate_array(
   const exprt &expr,
diff --git a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp
@@ -14,6 +14,7 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_types.h>
 
 #include <util/fresh_symbol.h>
+#include <util/goto_instruction_code.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/symbol_table_base.h>
diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
@@ -12,6 +12,7 @@ Date:   June 2017
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/goto_instruction_code.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp
@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_bytecode_typecheck.h"
 
-#include <util/std_code.h>
+#include <util/goto_instruction_code.h>
 
 void java_bytecode_typecheckt::typecheck_code(codet &code)
 {
diff --git a/jbmc/src/java_bytecode/lift_clinit_calls.cpp b/jbmc/src/java_bytecode/lift_clinit_calls.cpp
@@ -13,6 +13,7 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_static_initializers.h>
 
 #include <util/expr_iterator.h>
+#include <util/goto_instruction_code.h>
 
 #include <algorithm>
 
diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.h b/jbmc/unit/java-testing-utils/require_goto_statements.h
@@ -9,8 +9,8 @@ Author: Diffblue Ltd.
 /// \file
 /// Utilties for inspecting goto functions
 
+#include <util/goto_instruction_code.h>
 #include <util/optional.h>
-#include <util/std_code.h>
 
 #include <regex>
 
diff --git a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp
@@ -7,14 +7,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 \*******************************************************************/
 
 #include <java_bytecode/assignments_from_json.h>
-
 #include <java_bytecode/ci_lazy_methods_needed.h>
 #include <java_bytecode/java_bytecode_convert_class.h>
 #include <java_bytecode/java_types.h>
 #include <java_bytecode/java_utils.h>
+
 #include <testing-utils/expr_query.h>
 #include <testing-utils/use_catch.h>
+
 #include <util/arith_tools.h>
+#include <util/goto_instruction_code.h>
 #include <util/json.h>
 #include <util/symbol_table.h>
 
diff --git a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp
@@ -16,6 +16,7 @@ Author: Diffblue Ltd.
 #include <testing-utils/use_catch.h>
 
 #include <util/arith_tools.h>
+#include <util/goto_instruction_code.h>
 #include <util/json.h>
 #include <util/symbol_table.h>
 
diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/fresh_symbol.h>
+#include <util/goto_instruction_code.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
+#include <util/goto_instruction_code.h>
 #include <util/mathematical_expr.h>
 #include <util/std_code.h>
 
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
+#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
 
 bool cpp_typecheckt::find_dtor(const symbolt &symbol) const
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 
diff --git a/src/goto-instrument/object_id.cpp b/src/goto-instrument/object_id.cpp
@@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "object_id.h"
 
+#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
-#include <util/std_code.h>
 
 enum class get_modet { LHS_R, LHS_W, READ };
 
diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp
@@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "destructor.h"
 
+#include <util/goto_instruction_code.h>
 #include <util/namespace.h>
-#include <util/std_code.h>
 
 code_function_callt get_destructor(
   const namespacet &ns,
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
@@ -18,10 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 
 #include <util/deprecate.h>
+#include <util/goto_instruction_code.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/source_location.h>
-#include <util/std_code.h>
 
 enum class validation_modet;
 
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
@@ -13,8 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // #include <langapi/language_util.h>
 
+#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
-#include <util/std_code.h>
 
 #include <util/invariant.h>
 
diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp
@@ -11,6 +11,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 
 #include "jsil_convert.h"
 
+#include <util/goto_instruction_code.h>
 #include <util/message.h>
 #include <util/symbol_table.h>
 
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
@@ -12,8 +12,8 @@ Author: Michael Tautschnig, tautschn@amazon.com
 #include "jsil_typecheck.h"
 
 #include <util/bitvector_types.h>
+#include <util/goto_instruction_code.h>
 #include <util/prefix.h>
-#include <util/std_code.h>
 #include <util/symbol_table.h>
 
 #include "expr2jsil.h"
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
@@ -11,7 +11,7 @@ extern char *yyjsiltext;
 #define YYSTYPE unsigned
 #define YYSTYPE_IS_TRIVIAL 1
 
-#include <util/std_code.h>
+#include <util/goto_instruction_code.h>
 #include <util/string_constant.h>
 
 #include "jsil_y.tab.h"
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/goto_instruction_code.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
@@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
+#include <util/goto_instruction_code.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
@@ -23,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol.h>
 
 #include <langapi/language_util.h>
-#include <util/c_types.h>
 
 const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank{};
 
diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp
@@ -13,6 +13,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 #include "converters/statement_list_types.h"
 
 #include <util/cprover_prefix.h>
+#include <util/goto_instruction_code.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
diff --git a/src/util/allocate_objects.h b/src/util/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 "std_code.h"
 
 /// Selects the kind of objects allocated
 enum class lifetimet
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
@@ -14,12 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "format_type.h"
+#include "goto_instruction_code.h"
 #include "ieee_float.h"
 #include "mathematical_expr.h"
 #include "mp_arith.h"
 #include "pointer_expr.h"
 #include "prefix.h"
-#include "std_code.h"
 #include "string_utils.h"
 
 #include <map>
diff --git a/src/util/goto_instruction_code.h b/src/util/goto_instruction_code.h
diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp
diff --git a/src/util/std_code.h b/src/util/std_code.h
diff --git a/src/util/validate_code.cpp b/src/util/validate_code.cpp

Original file line number	Diff line number	Diff line change
`@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]`
`11`	`11`
`12`	`12`	`#include "java_bytecode_typecheck.h"`
`13`	`13`
`14`		`-#include <util/std_code.h>`
	`14`	`+#include <util/goto_instruction_code.h>`
`15`	`15`
`16`	`16`	`void java_bytecode_typecheckt::typecheck_code(codet &code)`
`17`	`17`	`{`