From 848d182f31765d65f5cd6c80abf3a405de9afc65 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 22 Aug 2021 22:29:52 +0100 Subject: [PATCH] remove an include from goto-programs/goto_program.h This removes an unneeded include from goto-programs/goto_program.h, which is widely used. --- jbmc/src/java_bytecode/java_local_variable_table.cpp | 1 + jbmc/unit/java-testing-utils/require_goto_statements.cpp | 1 + .../java_trace_validation/java_trace_validation.cpp | 1 + src/analyses/local_bitvector_analysis.cpp | 1 + src/analyses/local_cfg.h | 2 ++ src/analyses/local_safe_pointers.cpp | 1 + src/analyses/local_safe_pointers.h | 2 ++ src/analyses/uncaught_exceptions_analysis.cpp | 1 + .../variable-sensitivity/abstract_environment.cpp | 1 + .../variable-sensitivity/variable_sensitivity_domain.cpp | 1 + src/cbmc/c_test_input_generator.cpp | 1 + src/goto-checker/symex_coverage.cpp | 1 + src/goto-instrument/cover_filter.cpp | 1 + src/goto-instrument/cover_instrument.h | 2 ++ src/goto-instrument/function_modifies.h | 2 ++ src/goto-instrument/splice_call.cpp | 1 + src/goto-instrument/wmm/fence.cpp | 1 + src/goto-instrument/wmm/shared_buffers.h | 3 ++- src/goto-programs/builtin_functions.cpp | 1 + src/goto-programs/goto_clean_expr.cpp | 1 + src/goto-programs/goto_convert_exceptions.cpp | 1 + src/goto-programs/goto_function.cpp | 2 ++ src/goto-programs/goto_functions.cpp | 2 ++ src/goto-programs/goto_functions.h | 2 ++ src/goto-programs/goto_inline_class.cpp | 1 + src/goto-programs/goto_program.cpp | 6 ++++++ src/goto-programs/goto_program.h | 8 ++------ src/goto-programs/graphml_witness.cpp | 1 + src/goto-programs/interpreter_class.h | 5 +++-- src/goto-programs/json_goto_trace.cpp | 1 + src/goto-programs/rebuild_goto_start_function.cpp | 2 +- src/goto-programs/remove_virtual_functions.cpp | 1 + src/goto-programs/remove_virtual_functions.h | 3 +++ src/goto-programs/string_abstraction.h | 2 ++ src/goto-symex/build_goto_trace.cpp | 1 + src/jsil/jsil_entry_point.cpp | 1 + src/json-symtab-language/json_symtab_language.h | 2 ++ src/pointer-analysis/value_set.cpp | 1 + src/pointer-analysis/value_set_analysis_fi.cpp | 2 ++ src/pointer-analysis/value_set_dereference.cpp | 1 + src/statement-list/statement_list_entry_point.cpp | 1 + src/statement-list/statement_list_entry_point.h | 2 +- unit/analyses/ai/ai_simplify_lhs.cpp | 3 ++- unit/analyses/does_remove_const/does_expr_lose_const.cpp | 1 + .../abstract_environment/to_predicate.cpp | 3 +++ .../variable-sensitivity/abstract_object/index_range.cpp | 1 + .../variable-sensitivity/abstract_object/merge.cpp | 1 + .../variable-sensitivity/constant_abstract_value/meet.cpp | 1 + .../constant_abstract_value/merge.cpp | 1 + .../constant_abstract_value/to_predicate.cpp | 3 +++ .../constant_pointer_abstract_object/to_predicate.cpp | 3 +++ unit/analyses/variable-sensitivity/eval-member-access.cpp | 3 +++ unit/analyses/variable-sensitivity/eval.cpp | 1 + .../full_array_abstract_object/maximum_length.cpp | 4 ++++ .../full_array_abstract_object/to_predicate.cpp | 3 +++ .../full_struct_abstract_object/to_predicate.cpp | 1 + .../interval_abstract_value/extremes-go-top.cpp | 2 ++ .../variable-sensitivity/interval_abstract_value/meet.cpp | 2 ++ .../interval_abstract_value/merge.cpp | 2 ++ .../interval_abstract_value/to_predicate.cpp | 3 +++ .../interval_abstract_value/widening_merge.cpp | 1 + .../value_expression_evaluation/assume.cpp | 2 ++ .../value_expression_evaluation/assume_prune.cpp | 1 + .../value_expression_evaluation/expression_evaluation.cpp | 2 ++ .../value_set_abstract_object/compacting.cpp | 1 + .../value_set_abstract_object/extremes-go-top.cpp | 4 +++- .../value_set_abstract_object/meet.cpp | 2 ++ .../value_set_abstract_object/merge.cpp | 1 + .../value_set_abstract_object/to_predicate.cpp | 3 +++ .../value_set_abstract_object/widening_merge.cpp | 1 + .../value_set_pointer_abstract_object/to_predicate.cpp | 3 +++ .../variable_sensitivity_domain/to_predicate.cpp | 3 +++ .../variable_sensitivity_test_helpers.cpp | 1 + unit/goto-programs/goto_program_assume.cpp | 1 + unit/goto-programs/goto_program_dead.cpp | 1 + unit/goto-programs/goto_program_declaration.cpp | 1 + unit/goto-programs/goto_program_function_call.cpp | 1 + unit/goto-programs/goto_program_goto_target.cpp | 1 + .../goto_program_symbol_type_table_consistency.cpp | 1 + unit/goto-programs/goto_program_table_consistency.cpp | 1 + unit/goto-programs/goto_trace_output.cpp | 4 ++++ unit/goto-symex/ssa_equation.cpp | 1 + unit/pointer-analysis/value_set.cpp | 1 + 83 files changed, 137 insertions(+), 13 deletions(-) diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index b70a7bb8dd6..e40fa80b410 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -16,6 +16,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include #include +#include #include diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 754819bbb92..f98f2dc111c 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -18,6 +18,7 @@ Author: Diffblue Ltd. #include #include #include +#include /// Expand value of a function to include all child codets /// \param function_value: The value of the function (e.g. got by looking up diff --git a/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp b/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp index fc8723704f6..b1128c25cf5 100644 --- a/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp +++ b/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp @@ -16,6 +16,7 @@ Author: Diffblue Ltd. #include #include +#include TEST_CASE("java trace validation", "[core][java_trace_validation]") { diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index f9146f5ebfb..80710f51890 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include void local_bitvector_analysist::flagst::print(std::ostream &out) const { diff --git a/src/analyses/local_cfg.h b/src/analyses/local_cfg.h index 9c80d0ea3ad..f5e36a17ad3 100644 --- a/src/analyses/local_cfg.h +++ b/src/analyses/local_cfg.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + class local_cfgt { public: diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index 178a11ab04b..2e6637103ae 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -14,6 +14,7 @@ Author: Diffblue Ltd #include #include #include +#include /// Return structure for `get_null_checked_expr` and /// `get_conditional_checked_expr` diff --git a/src/analyses/local_safe_pointers.h b/src/analyses/local_safe_pointers.h index 69d0cfaa356..497f06beadb 100644 --- a/src/analyses/local_safe_pointers.h +++ b/src/analyses/local_safe_pointers.h @@ -16,6 +16,8 @@ Author: Diffblue Ltd #include +#include + /// 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 diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index b6dc242c979..b46606f1f99 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -15,6 +15,7 @@ Author: Cristina David #include "uncaught_exceptions_analysis.h" #include +#include #include diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index 36bc92a48d3..a5cf83a86a9 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -14,6 +14,7 @@ #include #include #include +#include #include #include diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 072cdd3d69f..f6f3a3de855 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -11,6 +11,7 @@ Date: April 2016 #include "variable_sensitivity_domain.h" #include +#include #include diff --git a/src/cbmc/c_test_input_generator.cpp b/src/cbmc/c_test_input_generator.cpp index 1a9fbbb79c7..0b506a754c3 100644 --- a/src/cbmc/c_test_input_generator.cpp +++ b/src/cbmc/c_test_input_generator.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include +#include #include #include diff --git a/src/goto-checker/symex_coverage.cpp b/src/goto-checker/symex_coverage.cpp index 5c4694c2b3f..4a37262bb99 100644 --- a/src/goto-checker/symex_coverage.cpp +++ b/src/goto-checker/symex_coverage.cpp @@ -19,6 +19,7 @@ Date: March 2016 #include #include +#include #include #include diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp index 26b2f7d2c4f..df765718bf3 100644 --- a/src/goto-instrument/cover_filter.cpp +++ b/src/goto-instrument/cover_filter.cpp @@ -12,6 +12,7 @@ Author: Peter Schrammel #include "cover_filter.h" #include +#include #include diff --git a/src/goto-instrument/cover_instrument.h b/src/goto-instrument/cover_instrument.h index bda1b1289c1..a898fbe52f5 100644 --- a/src/goto-instrument/cover_instrument.h +++ b/src/goto-instrument/cover_instrument.h @@ -14,6 +14,8 @@ Author: Peter Schrammel #include +#include + #include enum class coverage_criteriont; diff --git a/src/goto-instrument/function_modifies.h b/src/goto-instrument/function_modifies.h index 2dff92bcf0a..fa235955069 100644 --- a/src/goto-instrument/function_modifies.h +++ b/src/goto-instrument/function_modifies.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + class goto_functionst; class local_may_aliast; diff --git a/src/goto-instrument/splice_call.cpp b/src/goto-instrument/splice_call.cpp index 8a95d5804e3..4d125406e37 100644 --- a/src/goto-instrument/splice_call.cpp +++ b/src/goto-instrument/splice_call.cpp @@ -17,6 +17,7 @@ Date: July 2017 #include #include +#include #include diff --git a/src/goto-instrument/wmm/fence.cpp b/src/goto-instrument/wmm/fence.cpp index 329a0238b02..cead99e2b48 100644 --- a/src/goto-instrument/wmm/fence.cpp +++ b/src/goto-instrument/wmm/fence.cpp @@ -14,6 +14,7 @@ Date: February 2012 #include "fence.h" #include +#include bool is_fence( const goto_programt::instructiont &instruction, diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h index 19d9082cda4..241bc76f47d 100644 --- a/src/goto-instrument/wmm/shared_buffers.h +++ b/src/goto-instrument/wmm/shared_buffers.h @@ -14,9 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include +#include #include +#include #include "wmm.h" diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 55b8404b52c..404f4a4a88e 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index d3871792cbd..f99e41a2fbc 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include symbol_exprt goto_convertt::make_compound_literal( const exprt &expr, diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index 1a54df81240..e485aabd0b0 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_class.h" #include +#include void goto_convertt::convert_msc_try_finally( const codet &code, diff --git a/src/goto-programs/goto_function.cpp b/src/goto-programs/goto_function.cpp index f613f4f9ee1..6a97413f7ad 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -13,6 +13,8 @@ Date: May 2018 #include "goto_function.h" +#include + /// 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( diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index 8b0c26b6770..789daedc074 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -13,6 +13,8 @@ Date: June 2003 #include "goto_functions.h" +#include + #include void goto_functionst::compute_location_numbers() diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index 29f97189e74..01a73e7e625 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -18,6 +18,8 @@ Date: June 2003 #include +#include + /// A collection of goto functions class goto_functionst { diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 670888a6202..eb8cea23618 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include void goto_inlinet::parameter_assignments( const goto_programt::targett target, diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 000cc827785..30a836ba8a1 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -21,10 +21,16 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include +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: /// ``` diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index d4660e39bb5..45e147a9f67 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include enum class validation_modet; @@ -776,11 +775,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( diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index b03c0b50cda..284597bcb50 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening #include #include #include +#include #include #include diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 58dac3a193a..bf3fbcb41d3 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -16,9 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include #include +#include +#include +#include #include "goto_functions.h" #include "goto_trace.h" diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index c8dcab49a71..e145226c043 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening #include #include +#include #include diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index 88e28ffa285..bbb29e8089c 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -12,7 +12,7 @@ Author: Thomas Kiley, thomas@diffblue.com #include "rebuild_goto_start_function.h" #include -#include +#include #include #include diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 9459f593848..76a400c8d46 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "class_hierarchy.h" #include "class_identifier.h" diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h index 365828ce71e..e332a49dc93 100644 --- a/src/goto-programs/remove_virtual_functions.h +++ b/src/goto-programs/remove_virtual_functions.h @@ -20,10 +20,13 @@ Date: April 2016 #include "goto_program.h" +#include + 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 diff --git a/src/goto-programs/string_abstraction.h b/src/goto-programs/string_abstraction.h index 5bf7e58eaae..ede50ceca1d 100644 --- a/src/goto-programs/string_abstraction.h +++ b/src/goto-programs/string_abstraction.h @@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_function.h" +#include + class goto_functionst; class goto_modelt; class message_handlert; diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index f39484a1fdd..9950261a7ae 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening #include #include #include +#include #include diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 5cb7d3daaa3..57d2d7a049e 100644 --- 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 #include #include +#include #include #include diff --git a/src/json-symtab-language/json_symtab_language.h b/src/json-symtab-language/json_symtab_language.h index 521a3a8d50b..20508242ca0 100644 --- a/src/json-symtab-language/json_symtab_language.h +++ b/src/json-symtab-language/json_symtab_language.h @@ -16,8 +16,10 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include + #include #include +#include class json_symtab_languaget : public languaget { diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index ab470f94bfc..6554aa9132e 100644 --- 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 #include #include +#include #ifdef DEBUG #include diff --git a/src/pointer-analysis/value_set_analysis_fi.cpp b/src/pointer-analysis/value_set_analysis_fi.cpp index e091188541c..1e250a6038c 100644 --- a/src/pointer-analysis/value_set_analysis_fi.cpp +++ b/src/pointer-analysis/value_set_analysis_fi.cpp @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "value_set_analysis_fi.h" +#include + void value_set_analysis_fit::initialize( const goto_programt &goto_program) { diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 525c62c6b6f..b716837fe01 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -30,6 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include diff --git a/src/statement-list/statement_list_entry_point.cpp b/src/statement-list/statement_list_entry_point.cpp index c9969611da3..a9e37fab892 100644 --- a/src/statement-list/statement_list_entry_point.cpp +++ b/src/statement-list/statement_list_entry_point.cpp @@ -21,6 +21,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include #include #include +#include /// Postfix for the artificial data block that is created when calling a main /// symbol that is a function block. diff --git a/src/statement-list/statement_list_entry_point.h b/src/statement-list/statement_list_entry_point.h index a74bf1423dc..0638a9e8a40 100644 --- a/src/statement-list/statement_list_entry_point.h +++ b/src/statement-list/statement_list_entry_point.h @@ -12,8 +12,8 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #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 diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index 325527819d9..398a9a069a4 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -20,8 +20,9 @@ Author: Diffblue Ltd. #include #include #include -#include #include +#include +#include class constant_simplification_mockt:public ai_domain_baset { diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/unit/analyses/does_remove_const/does_expr_lose_const.cpp index 3bb3471603e..d1a41bdf867 100644 --- a/unit/analyses/does_remove_const/does_expr_lose_const.cpp +++ b/unit/analyses/does_remove_const/does_expr_lose_const.cpp @@ -15,6 +15,7 @@ Author: Diffblue Ltd. #include #include #include +#include #include diff --git a/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp index 1102dc5f768..0fbaa685efc 100644 --- a/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp @@ -8,10 +8,13 @@ #include #include + #include + #include #include #include +#include SCENARIO( "abstract_environment to predicate", diff --git a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp index 5905b2c7044..3f3e1717ec5 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp @@ -15,6 +15,7 @@ #include #include +#include SCENARIO( "index_range for constant_abstract_values" diff --git a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp index 22891493a92..ca45f8100cb 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp @@ -15,6 +15,7 @@ #include #include +#include SCENARIO( "merge abstract object", diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp index bc9a36a8ede..59436db82aa 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp @@ -12,6 +12,7 @@ #include #include +#include static std::shared_ptr meet(abstract_object_pointert const &op1, abstract_object_pointert const &op2) diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index 4e7f873bebd..bdc6d976e7d 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -12,6 +12,7 @@ #include #include +#include static merge_result merge(abstract_object_pointert op1, abstract_object_pointert op2) diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp index a7bcf1899ba..83b40ad7bfe 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp @@ -8,9 +8,12 @@ #include #include + #include + #include #include +#include SCENARIO( "constant_abstract_value to predicate", diff --git a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp index 468767c2080..93a7e78590b 100644 --- a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp @@ -8,10 +8,13 @@ #include #include + #include + #include #include #include +#include SCENARIO( "constant_pointer_abstract_object to predicate", diff --git a/unit/analyses/variable-sensitivity/eval-member-access.cpp b/unit/analyses/variable-sensitivity/eval-member-access.cpp index bcf69aa2c86..feeea753bac 100644 --- a/unit/analyses/variable-sensitivity/eval-member-access.cpp +++ b/unit/analyses/variable-sensitivity/eval-member-access.cpp @@ -5,14 +5,17 @@ Author: Jez Higgins \*******************************************************************/ + #include #include #include #include #include + #include #include +#include void test_array( std::vector contents, diff --git a/unit/analyses/variable-sensitivity/eval.cpp b/unit/analyses/variable-sensitivity/eval.cpp index 6161674f281..fdbf07363d9 100644 --- a/unit/analyses/variable-sensitivity/eval.cpp +++ b/unit/analyses/variable-sensitivity/eval.cpp @@ -7,6 +7,7 @@ #include #include #include +#include static symbolt simple_symbol(const irep_idt &identifier, const typet &type) { diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp index 046219e105d..68ca952d934 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp @@ -7,12 +7,16 @@ \*******************************************************************/ #include "array_builder.h" + #include #include + #include + #include #include #include +#include using abstract_object_ptrt = std::shared_ptr; diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp index 4d999ab1b16..263244fcbc1 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp @@ -11,8 +11,11 @@ #include #include + #include +#include + SCENARIO( "array to predicate", "[core][analyses][variable-sensitivity][full_array_abstract_object][to_" diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp index 5f145b03d65..42431368313 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp @@ -16,6 +16,7 @@ #include #include +#include SCENARIO( "struct to predicate", diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp index 0a188e78314..b13541c5db6 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp @@ -13,8 +13,10 @@ #include #include + #include #include +#include static void verify_extreme_interval(typet type, abstract_environmentt &env, namespacet &ns) diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp index 198e78f0da1..69398581a3d 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp @@ -14,8 +14,10 @@ #include #include + #include #include +#include static std::shared_ptr meet(abstract_object_pointert const &op1, abstract_object_pointert const &op2) diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp index a8e97f2faa5..af83d5c5aa5 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp @@ -8,10 +8,12 @@ #include #include + #include #include #include +#include static merge_result merge(abstract_object_pointert op1, abstract_object_pointert op2) diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp index 0f8ee5b8fea..46ecd73dbb5 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp @@ -8,9 +8,12 @@ #include #include + #include + #include #include +#include SCENARIO( "interval_abstract_value to predicate", diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp index 8a9641aa729..8622c08b831 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp @@ -12,6 +12,7 @@ #include #include +#include static merge_result widening_merge( const abstract_object_pointert &op1, diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp index a2c2b0b9d0e..9441a748af7 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp @@ -8,10 +8,12 @@ #include #include + #include #include #include +#include exprt binary_expression( dstringt const &exprId, diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp index c52cde4a4a0..16858b9dec0 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp @@ -12,6 +12,7 @@ #include #include +#include static void ASSUME_TRUE( symbol_exprt const &x, diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp index 38525d59083..e13e668437a 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -8,10 +8,12 @@ #include #include + #include #include #include +#include SCENARIO( "value expression evaluation", diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp index 956364b6220..5d298eaa230 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp @@ -19,6 +19,7 @@ #include #include #include +#include SCENARIO( "compacting value sets", diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp index 2b18b941ffa..8bebf537a07 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp @@ -10,11 +10,13 @@ #include #include #include +#include + #include -#include #include #include +#include SCENARIO( "value-sets spanning min-max go TOP", diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp index adef5bb9303..67c44589c26 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp @@ -14,8 +14,10 @@ #include #include + #include #include +#include static std::shared_ptr meet(abstract_object_pointert const &op1, abstract_object_pointert const &op2) diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp index 887ab0d505f..126398ec5ea 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp @@ -14,6 +14,7 @@ #include #include +#include static merge_result merge(abstract_object_pointert op1, abstract_object_pointert op2) diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp index dec14931876..c3f2bbc139b 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp @@ -8,9 +8,12 @@ #include #include + #include + #include #include +#include SCENARIO( "value_set_abstract_object to predicate", diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp index c23c4e13c6e..a64e2e541db 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp @@ -12,6 +12,7 @@ #include #include +#include static merge_result widening_merge(abstract_object_pointert op1, abstract_object_pointert op2) diff --git a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp index 16c796e3df6..0869d2eeefb 100644 --- a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp @@ -9,10 +9,13 @@ #include #include #include + #include + #include #include #include +#include template std::shared_ptr make_vsp(Args &&... args) diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp index 7d40afe4718..ab9a07e2da5 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp @@ -9,10 +9,13 @@ #include #include #include + #include + #include #include #include +#include SCENARIO( "variable_sensitivity_domain to predicate", diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index b3a4e2c236f..a2817ffb6c4 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -22,6 +22,7 @@ #include #include #include +#include std::shared_ptr make_constant(exprt val, abstract_environmentt &env, namespacet &ns) diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp index c5d0573daf6..f9147e8ca9f 100644 --- a/unit/goto-programs/goto_program_assume.cpp +++ b/unit/goto-programs/goto_program_assume.cpp @@ -10,6 +10,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp index 3d7edbc5d89..36aed6daaff 100644 --- a/unit/goto-programs/goto_program_dead.cpp +++ b/unit/goto-programs/goto_program_dead.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp index aa381d1b88c..4f4d1292e76 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index 5ad47188839..978f517d5d9 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index ac23fa0edd3..5033304ece6 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -10,6 +10,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp index 8f575edc7fa..1a8e942137d 100644 --- a/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp +++ b/unit/goto-programs/goto_program_symbol_type_table_consistency.cpp @@ -10,6 +10,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_program_table_consistency.cpp b/unit/goto-programs/goto_program_table_consistency.cpp index 36207ce116c..8e381448bec 100644 --- a/unit/goto-programs/goto_program_table_consistency.cpp +++ b/unit/goto-programs/goto_program_table_consistency.cpp @@ -10,6 +10,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/goto-programs/goto_trace_output.cpp b/unit/goto-programs/goto_trace_output.cpp index 5e7604ad19f..4d8ea1d2ed7 100644 --- a/unit/goto-programs/goto_trace_output.cpp +++ b/unit/goto-programs/goto_trace_output.cpp @@ -8,9 +8,13 @@ Author: Diffblue Ltd. #include #include + #include + #include +#include + SCENARIO( "Output trace with nil lhs object", "[core][goto-programs][goto_trace]") diff --git a/unit/goto-symex/ssa_equation.cpp b/unit/goto-symex/ssa_equation.cpp index 3077106a9bb..f86b3d89f9c 100644 --- a/unit/goto-symex/ssa_equation.cpp +++ b/unit/goto-symex/ssa_equation.cpp @@ -10,6 +10,7 @@ Author: Diffblue Ltd. #include #include +#include #include diff --git a/unit/pointer-analysis/value_set.cpp b/unit/pointer-analysis/value_set.cpp index f04ab6540b0..f9bae41ff60 100644 --- a/unit/pointer-analysis/value_set.cpp +++ b/unit/pointer-analysis/value_set.cpp @@ -15,6 +15,7 @@ Author: Diffblue Ltd. #include #include +#include static bool object_descriptor_matches( const exprt &descriptor_expr, const exprt &target)