Merge pull request #6312 from diffblue/goto_program_include

remove an include from goto-programs/goto_program.h

Author: kroening

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -16,6 +16,7 @@ Author: Chris Smowton, [email protected]
 #include <util/arith_tools.h>
 #include <util/invariant.h>
 #include <util/string2int.h>
+#include <util/symbol_table.h>
 
 #include <iostream>
 

jbmc/unit/java-testing-utils/require_goto_statements.cpp

@@ -18,6 +18,7 @@ Author: Diffblue Ltd.
 #include <util/expr_util.h>
 #include <util/pointer_expr.h>
 #include <util/suffix.h>
+#include <util/symbol_table.h>
 
 /// Expand value of a function to include all child codets
 /// \param function_value: The value of the function (e.g. got by looking up

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -16,6 +16,7 @@ Author: Diffblue Ltd.
 
 #include <util/byte_operators.h>
 #include <util/pointer_expr.h>
+#include <util/symbol_table.h>
 
 TEST_CASE("java trace validation", "[core][java_trace_validation]")
 {

src/analyses/local_bitvector_analysis.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
+#include <util/symbol_table.h>
 
 void local_bitvector_analysist::flagst::print(std::ostream &out) const
 {

src/analyses/local_cfg.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_program.h>
 
+#include <map>
+
 class local_cfgt
 {
 public:

src/analyses/local_safe_pointers.cpp

@@ -14,6 +14,7 @@ Author: Diffblue Ltd
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
+#include <util/symbol_table.h>
 
 /// Return structure for `get_null_checked_expr` and
 /// `get_conditional_checked_expr`

src/analyses/local_safe_pointers.h

@@ -16,6 +16,8 @@ Author: Diffblue Ltd
 
 #include <util/pointer_expr.h>
 
+#include <map>
+
 /// A very simple, cheap analysis to determine when dereference operations are
 /// trivially guarded by a check against a null pointer access.
 /// In the interests of a very cheap analysis we only search for very local

src/analyses/uncaught_exceptions_analysis.cpp

@@ -15,6 +15,7 @@ Author: Cristina David
 #include "uncaught_exceptions_analysis.h"
 
 #include <util/namespace.h>
+#include <util/symbol_table.h>
 
 #include <goto-programs/goto_functions.h>
 

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -14,6 +14,7 @@
 #include <util/simplify_expr.h>
 #include <util/simplify_expr_class.h>
 #include <util/simplify_utils.h>
+#include <util/symbol_table.h>
 
 #include <algorithm>
 #include <map>

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -11,6 +11,7 @@ Date: April 2016
 #include "variable_sensitivity_domain.h"
 
 #include <util/cprover_prefix.h>
+#include <util/symbol_table.h>
 
 #include <algorithm>
 

src/cbmc/c_test_input_generator.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/json_stream.h>
 #include <util/options.h>
 #include <util/string_utils.h>
+#include <util/symbol.h>
 #include <util/ui_message.h>
 #include <util/xml.h>
 

src/goto-checker/symex_coverage.cpp

@@ -19,6 +19,7 @@ Date: March 2016
 #include <iostream>
 
 #include <util/string2int.h>
+#include <util/symbol.h>
 #include <util/xml.h>
 
 #include <langapi/language_util.h>

src/goto-instrument/cover_filter.cpp

@@ -12,6 +12,7 @@ Author: Peter Schrammel
 #include "cover_filter.h"
 
 #include <util/prefix.h>
+#include <util/symbol.h>
 
 #include <linking/static_lifetime_init.h>
 

src/goto-instrument/cover_instrument.h

@@ -14,6 +14,8 @@ Author: Peter Schrammel
 
 #include <memory>
 
+#include <util/symbol_table.h>
+
 #include <goto-programs/goto_program.h>
 
 enum class coverage_criteriont;

src/goto-instrument/function_modifies.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_program.h>
 
+#include <map>
+
 class goto_functionst;
 class local_may_aliast;
 

src/goto-instrument/splice_call.cpp

@@ -17,6 +17,7 @@ Date: July 2017
 
 #include <util/message.h>
 #include <util/string_utils.h>
+#include <util/symbol_table.h>
 
 #include <goto-programs/goto_functions.h>
 

src/goto-instrument/wmm/fence.cpp

@@ -14,6 +14,7 @@ Date: February 2012
 #include "fence.h"
 
 #include <util/namespace.h>
+#include <util/symbol.h>
 
 bool is_fence(
   const goto_programt::instructiont &instruction,

src/goto-instrument/wmm/shared_buffers.h

@@ -14,9 +14,10 @@ Author: Daniel Kroening, [email protected]
 #include <set>
 
 #include <goto-programs/goto_program.h>
-#include <util/namespace.h>
 #include <util/cprover_prefix.h>
+#include <util/namespace.h>
 #include <util/prefix.h>
+#include <util/symbol_table.h>
 
 #include "wmm.h"
 

src/goto-programs/builtin_functions.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/prefix.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
+#include <util/symbol_table.h>
 
 #include <langapi/language_util.h>
 

src/goto-programs/goto_clean_expr.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/fresh_symbol.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
+#include <util/symbol.h>
 
 symbol_exprt goto_convertt::make_compound_literal(
   const exprt &expr,

src/goto-programs/goto_convert_exceptions.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "goto_convert_class.h"
 
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 void goto_convertt::convert_msc_try_finally(
   const codet &code,

src/goto-programs/goto_function.cpp

@@ -13,6 +13,8 @@ Date: May 2018
 
 #include "goto_function.h"
 
+#include <util/symbol.h>
+
 /// Return in \p dest the identifiers of the local variables declared in the \p
 /// goto_function and the identifiers of the paramters of the \p goto_function.
 void get_local_identifiers(

src/goto-programs/goto_functions.cpp

@@ -13,6 +13,8 @@ Date: June 2003
 
 #include "goto_functions.h"
 
+#include <util/symbol.h>
+
 #include <algorithm>
 
 void goto_functionst::compute_location_numbers()

src/goto-programs/goto_functions.h

@@ -18,6 +18,8 @@ Date: June 2003
 
 #include <util/cprover_prefix.h>
 
+#include <map>
+
 /// A collection of goto functions
 class goto_functionst
 {

src/goto-programs/goto_inline_class.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/invariant.h>
 #include <util/std_code.h>
+#include <util/symbol.h>
 
 void goto_inlinet::parameter_assignments(
   const goto_programt::targett target,

src/goto-programs/goto_program.cpp

@@ -21,10 +21,16 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 #include <util/validate.h>
 
 #include <langapi/language_util.h>
 
+std::ostream &goto_programt::output(std::ostream &out) const
+{
+  return output(namespacet(symbol_tablet()), irep_idt(), out);
+}
+
 /// Writes to \p out a two/three line string representation of a given
 /// \p instruction. The output is of the format:
 /// ```

src/goto-programs/goto_program.h

@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/namespace.h>
 #include <util/source_location.h>
 #include <util/std_code.h>
-#include <util/symbol_table.h>
 
 enum class validation_modet;
 
@@ -777,11 +776,8 @@ class goto_programt
     const irep_idt &identifier,
     std::ostream &out) const;
 
-  /// Output goto-program to given stream
-  std::ostream &output(std::ostream &out) const
-  {
-    return output(namespacet(symbol_tablet()), irep_idt(), out);
-  }
+  /// Output goto-program to given stream, using an empty symbol table
+  std::ostream &output(std::ostream &out) const;
 
   /// Output a single instruction
   std::ostream &output_instruction(

src/goto-programs/graphml_witness.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
 #include <util/string_constant.h>
+#include <util/symbol_table.h>
 
 #include <langapi/language_util.h>
 #include <langapi/mode.h>

src/goto-programs/interpreter_class.h

@@ -16,9 +16,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/invariant.h>
-#include <util/std_types.h>
-#include <util/sparse_vector.h>
 #include <util/message.h>
+#include <util/sparse_vector.h>
+#include <util/std_types.h>
+#include <util/symbol_table.h>
 
 #include "goto_functions.h"
 #include "goto_trace.h"

src/goto-programs/json_goto_trace.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening
 
 #include <util/invariant.h>
 #include <util/simplify_expr.h>
+#include <util/symbol.h>
 
 #include <langapi/language_util.h>
 

src/goto-programs/rebuild_goto_start_function.cpp

@@ -12,7 +12,7 @@ Author: Thomas Kiley, [email protected]
 #include "rebuild_goto_start_function.h"
 
 #include <util/prefix.h>
-#include <util/symbol.h>
+#include <util/symbol_table.h>
 
 #include <langapi/mode.h>
 #include <langapi/language.h>

src/goto-programs/remove_virtual_functions.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/prefix.h>
+#include <util/symbol_table.h>
 
 #include "class_hierarchy.h"
 #include "class_identifier.h"

src/goto-programs/remove_virtual_functions.h

@@ -20,10 +20,13 @@ Date: April 2016
 
 #include "goto_program.h"
 
+#include <map>
+
 class class_hierarchyt;
 class goto_functionst;
 class goto_model_functiont;
 class goto_modelt;
+class symbol_tablet;
 class symbol_table_baset;
 
 // For all of the following the class-hierarchy and non-class-hierarchy

src/goto-programs/string_abstraction.h

@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_function.h"
 
+#include <map>
+
 class goto_functionst;
 class goto_modelt;
 class message_handlert;

src/goto-symex/build_goto_trace.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/simplify_expr.h>
+#include <util/symbol.h>
 
 #include <goto-programs/goto_functions.h>
 

src/jsil/jsil_entry_point.cpp

@@ -15,6 +15,7 @@ Author: Michael Tautschnig, [email protected]
 #include <util/config.h>
 #include <util/message.h>
 #include <util/range.h>
+#include <util/symbol_table.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_functions.h>

src/json-symtab-language/json_symtab_language.h

@@ -16,8 +16,10 @@ Author: Chris Smowton, [email protected]
 
 #include <goto-programs/goto_functions.h>
 #include <langapi/language.h>
+
 #include <util/json.h>
 #include <util/make_unique.h>
+#include <util/symbol_table.h>
 
 class json_symtab_languaget : public languaget
 {

src/pointer-analysis/value_set.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/prefix.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
+#include <util/symbol_table.h>
 
 #ifdef DEBUG
 #include <iostream>

src/pointer-analysis/value_set_analysis_fi.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "value_set_analysis_fi.h"
 
+#include <util/symbol_table.h>
+
 void value_set_analysis_fit::initialize(
   const goto_programt &goto_program)
 {

src/pointer-analysis/value_set_dereference.cpp

@@ -30,6 +30,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_predicates.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
+#include <util/symbol_table.h>
 
 #include <deque>
 

src/statement-list/statement_list_entry_point.cpp

@@ -21,6 +21,7 @@ Author: Matthias Weiss, [email protected]
 #include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
+#include <util/symbol_table.h>
 
 /// Postfix for the artificial data block that is created when calling a main
 /// symbol that is a function block.

src/statement-list/statement_list_entry_point.h

@@ -12,8 +12,8 @@ Author: Matthias Weiss, [email protected]
 #ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_ENTRY_POINT_H
 #define CPROVER_STATEMENT_LIST_STATEMENT_LIST_ENTRY_POINT_H
 
-class symbol_tablet;
 class message_handlert;
+class symbol_tablet;
 
 /// Creates a new entry point for the Statement List language.
 /// \param [out] symbol_table: Symbol table of the current TIA program. Gets

unit/analyses/ai/ai_simplify_lhs.cpp

@@ -20,8 +20,9 @@ Author: Diffblue Ltd.
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/namespace.h>
-#include <util/ui_message.h>
 #include <util/simplify_expr.h>
+#include <util/symbol_table.h>
+#include <util/ui_message.h>
 
 class constant_simplification_mockt:public ai_domain_baset
 {