Merge pull request #6386 from diffblue/goto_instruction_code

Separate header file for goto-instruction codet types

Author: kroening

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>
 

jbmc/src/java_bytecode/code_with_references.cpp

@@ -8,7 +8,9 @@ Author: Romain Brenguier, [email protected]
 
 #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,

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>

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>
 

jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp

@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_bytecode_typecheck.h"
 
-#include <util/std_code.h>
+#include <util/goto_instruction_code.h>
 
 void java_bytecode_typecheckt::typecheck_code(codet &code)
 {

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>
 

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>
 

jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp

@@ -7,14 +7,16 @@ Author: Romain Brenguier, [email protected]
 \*******************************************************************/
 
 #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>
 

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>
 

src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #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>

src/ansi-c/c_typecheck_type.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #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>

src/ansi-c/expr2c_class.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 
 #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>
 

src/cpp/cpp_typecheck_constructor.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #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>
 

src/cpp/cpp_typecheck_destructor.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_typecheck.h"
 
+#include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
 
 bool cpp_typecheckt::find_dtor(const symbolt &symbol) const

src/cpp/cpp_typecheck_initializer.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #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>
 

src/goto-instrument/object_id.cpp

@@ -11,8 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #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 };
 

src/goto-programs/destructor.cpp

@@ -11,8 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #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,

src/goto-programs/goto_program.h

@@ -18,10 +18,10 @@ Author: Daniel Kroening, [email protected]
 #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;
 

src/goto-programs/wp.cpp

@@ -13,8 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 // #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>
 

src/jsil/jsil_convert.cpp

@@ -11,6 +11,7 @@ Author: Michael Tautschnig, [email protected]
 
 #include "jsil_convert.h"
 
+#include <util/goto_instruction_code.h>
 #include <util/message.h>
 #include <util/symbol_table.h>
 

src/jsil/jsil_typecheck.cpp

@@ -12,8 +12,8 @@ Author: Michael Tautschnig, [email protected]
 #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"

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"

src/linking/static_lifetime_init.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #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>

src/pointer-analysis/value_set_fi.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 
 #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, [email protected]
 #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{};
 

src/statement-list/statement_list_typecheck.cpp

@@ -13,6 +13,7 @@ Author: Matthias Weiss, [email protected]
 #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>

src/util/allocate_objects.h

@@ -9,9 +9,9 @@ Author: Daniel Kroening, [email protected]
 #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

src/util/format_expr.cpp

@@ -14,12 +14,12 @@ Author: Daniel Kroening, [email protected]
 #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>