Merge pull request #6405 from diffblue/std_code_include

kroening · web-flow · commit 708331332507 · 2021-10-22T10:14:45.000+01:00
goto_program.h no longer includes std_code.h
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/expanding_vector.h>
 #include <util/message.h>
+#include <util/std_code.h>
 #include <util/std_expr.h>
 
 #include <analyses/cfg_dominators.h>
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_typecheck.h"
 
 #include <util/goto_instruction_code.h>
+#include <util/std_code.h>
 
 void java_bytecode_typecheckt::typecheck_code(codet &code)
 {
diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp
@@ -22,6 +22,7 @@ Author: Peter Schrammel
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
 #include <util/pointer_offset_size.h>
+#include <util/std_code.h>
 
 class remove_java_newt
 {
diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -14,6 +14,8 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
+#include <util/std_code.h>
+
 #include <algorithm>
 #include <regex>
 
diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp
@@ -17,6 +17,7 @@ Author: Diffblue Ltd.
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 #include <util/suffix.h>
 #include <util/symbol_table.h>
 
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
@@ -25,6 +25,7 @@ Author: Peter Schrammel
 #include <util/ieee_float.h>
 #include <util/mathematical_types.h>
 #include <util/simplify_expr.h>
+#include <util/std_code.h>
 
 #include <langapi/language_util.h>
 
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -31,6 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
+#include <util/std_code.h>
 #include <util/std_expr.h>
 
 #include <langapi/language.h>
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp
@@ -10,9 +10,11 @@
 #include "data_dependency_context.h"
 
 #include <langapi/language_util.h>
+
 #include <util/container_utils.h>
 #include <util/json.h>
 #include <util/json_irep.h>
+#include <util/std_code.h>
 
 /**
  * Evaluate an expression and accumulate all the data dependencies
diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp
@@ -17,6 +17,7 @@ Date:   December 2014
 
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 #include <util/string_constant.h>
 
 #include <goto-programs/goto_model.h>
diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
+#include <util/std_code.h>
 #include <util/string_constant.h>
 
 #include <goto-programs/class_hierarchy.h>
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
@@ -15,9 +15,10 @@ Author: Matt Lewis
 
 #include <goto-programs/goto_functions.h>
 
-#include <util/std_expr.h>
 #include <util/arith_tools.h>
 #include <util/find_symbols.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
 
 #include <iostream>
 #include <list>
diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h
@@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/natural_loops.h>
 
+#include <util/std_code.h>
+
 class goto_program2codet
 {
   typedef std::list<irep_idt> id_listt;
diff --git a/src/goto-instrument/havoc_utils.cpp b/src/goto-instrument/havoc_utils.cpp
@@ -16,6 +16,7 @@ Date: July 2021
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 
 void havoc_utilst::append_full_havoc_code(
   const source_locationt location,
diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp
@@ -14,6 +14,7 @@ Date: September 2011
 #include "interrupt.h"
 
 #include <util/range.h>
+#include <util/std_code.h>
 
 #include <linking/static_lifetime_init.h>
 
diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp
@@ -20,6 +20,7 @@ Date: November 2011
 #include "nondet_static.h"
 
 #include <util/prefix.h>
+#include <util/std_code.h>
 
 #include <goto-programs/goto_model.h>
 
diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp
@@ -17,6 +17,7 @@ Date: September 2011
 #include <util/fresh_symbol.h>
 #include <util/options.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/string_utils.h>
 #include <util/symbol_table.h>
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 
 #include <linking/static_lifetime_init.h>
 
diff --git a/src/goto-programs/allocate_objects.h b/src/goto-programs/allocate_objects.h
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/goto_instruction_code.h>
 #include <util/namespace.h>
 #include <util/source_location.h>
+#include <util/std_code.h>
 
 /// Selects the kind of objects allocated
 enum class lifetimet
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/format_type.h>
 #include <util/invariant.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 #include <util/validate.h>
@@ -31,6 +32,13 @@ std::ostream &goto_programt::output(std::ostream &out) const
   return output(namespacet(symbol_tablet()), irep_idt(), out);
 }
 
+goto_programt::instructiont goto_programt::make_incomplete_goto(
+  const code_gotot &_code,
+  const source_locationt &l)
+{
+  return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
+}
+
 /// Writes to \p out a two/three line string representation of a given
 /// \p instruction. The output is of the format:
 /// ```
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/namespace.h>
 #include <util/source_location.h>
 
+class code_gotot;
 enum class validation_modet;
 
 /// The type of an instruction in a GOTO program.
@@ -980,11 +981,8 @@ class goto_programt
   }
 
   static instructiont make_incomplete_goto(
-    const code_gotot &_code,
-    const source_locationt &l = source_locationt::nil())
-  {
-    return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
-  }
+    const code_gotot &,
+    const source_locationt & = source_locationt::nil());
 
   static instructiont make_goto(
     targett _target,
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_types.h>
 #include <util/message.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
 #include <util/string_container.h>
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
+#include <util/std_code.h>
 #include <util/string_container.h>
 
 #include <langapi/language_util.h>
diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp
@@ -12,6 +12,7 @@ Author: Daniel Poetzl
 #include "remove_calls_no_body.h"
 
 #include <util/invariant.h>
+#include <util/std_code.h>
 
 #include "goto_functions.h"
 
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/source_location.h>
+#include <util/std_code.h>
 #include <util/std_expr.h>
 
 #include <analyses/does_remove_const.h>
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
@@ -13,6 +13,7 @@ Date:   September 2009
 
 #include "remove_returns.h"
 
+#include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/suffix.h>
 
diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "remove_skip.h"
 #include "goto_model.h"
 
+#include <util/std_code.h>
+
 /// Determine whether the instruction is semantically equivalent to a skip
 /// (no-op).  This includes a skip, but also if(false) goto ..., goto next;
 ///  next: ..., and (void)0.
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_predicates.h>
+#include <util/std_code.h>
 #include <util/string_constant.h>
 
 #include "goto_model.h"
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/goto_instruction_code.h>
 #include <util/pointer_expr.h>
+#include <util/std_code.h>
 
 #include <util/invariant.h>
 
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
+#include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 #include <util/simplify_utils.h>
+#include <util/std_code.h>
 #include <util/string_expr.h>
 #include <util/string_utils.h>
 
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/simplify_expr.h>
+#include <util/std_code.h>
 #include <util/string_constant.h>
 
 #include "path_storage.h"
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/range.h>
+#include <util/std_code.h>
 
 #include "expr_skeleton.h"
 #include "path_storage.h"
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/std_code.h>
 
 void goto_symext::havoc_rec(
   statet &state,
diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp
@@ -15,6 +15,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 #include <util/config.h>
 #include <util/message.h>
 #include <util/range.h>
+#include <util/std_code.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/adjust_float_expressions.h>
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
@@ -14,6 +14,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 #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/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/prefix.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
+#include <util/std_code.h>
 #include <util/symbol_table.h>
 
 #ifdef DEBUG
diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp
@@ -14,6 +14,7 @@ Author: Diffblue Ltd.
 #include <util/format_type.h>
 #include <util/json_irep.h>
 #include <util/json_stream.h>
+#include <util/std_code.h>
 
 solver_hardnesst::sat_hardnesst &solver_hardnesst::sat_hardnesst::
 operator+=(const solver_hardnesst::sat_hardnesst &other)
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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
@@ -9,7 +9,8 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
 #define CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
 
-#include "std_code.h"
+#include "std_code_base.h"
+#include "std_expr.h"
 
 /// A \ref codet representing an assignment in the program.
 /// For example, if an expression `e1` is represented as an \ref exprt `expr1`

Original file line number	Diff line number	Diff line change
`@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]`
`12`	`12`	`#include "java_bytecode_typecheck.h"`
`13`	`13`
`14`	`14`	`#include <util/goto_instruction_code.h>`
	`15`	`+#include <util/std_code.h>`
`15`	`16`
`16`	`17`	`void java_bytecode_typecheckt::typecheck_code(codet &code)`
`17`	`18`	`{`
Original file line number	Diff line number	Diff line change
`@@ -22,6 +22,7 @@ Author: Peter Schrammel`
`22`	`22`	`#include <util/c_types.h>`
`23`	`23`	`#include <util/expr_initializer.h>`
`24`	`24`	`#include <util/pointer_offset_size.h>`
	`25`	`+#include <util/std_code.h>`
`25`	`26`
`26`	`27`	`class remove_java_newt`
`27`	`28`	`{`