Merge pull request #8696 from tautschnig/contracts-cleanup-includes

Contracts instrumentation: cleanup unnecessary includes

Author: tautschnig

src/goto-instrument/contracts/contracts.cpp

@@ -14,27 +14,17 @@ Date: February 2016
 #include "contracts.h"
 
 #include <util/c_types.h>
-#include <util/exception_utils.h>
-#include <util/expr_util.h>
-#include <util/find_symbols.h>
 #include <util/format_expr.h>
 #include <util/fresh_symbol.h>
-#include <util/graph.h>
 #include <util/mathematical_expr.h>
-#include <util/message.h>
-#include <util/std_code.h>
 
 #include <goto-programs/goto_inline.h>
-#include <goto-programs/goto_program.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/unwindset.h>
 
 #include <analyses/local_may_alias.h>
-#include <ansi-c/c_expr.h>
-#include <goto-instrument/havoc_utils.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/unwind.h>
-#include <langapi/language_util.h>
 
 #include "cfg_info.h"
 #include "havoc_assigns_clause_targets.h"

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -9,43 +9,22 @@ Author: Remi Delmas, delmarsd@amazon.com
 #include "dfcc.h"
 
 #include <util/config.h>
-#include <util/expr_util.h>
-#include <util/format_expr.h>
-#include <util/format_type.h>
-#include <util/fresh_symbol.h>
-#include <util/mathematical_expr.h>
-#include <util/mathematical_types.h>
-#include <util/namespace.h>
-#include <util/pointer_expr.h>
-#include <util/pointer_offset_size.h>
-#include <util/pointer_predicates.h>
 #include <util/prefix.h>
-#include <util/std_expr.h>
 #include <util/string_utils.h>
 
-#include <goto-programs/goto_functions.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/goto_model.h>
-#include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
 
 #include <ansi-c/ansi_c_entry_point.h>
-#include <ansi-c/c_expr.h>
 #include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
-#include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <ansi-c/goto-conversion/link_to_library.h>
-#include <goto-instrument/contracts/cfg_info.h>
-#include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/generate_function_bodies.h>
 #include <goto-instrument/nondet_static.h>
-#include <langapi/language.h>
-#include <langapi/language_file.h>
-#include <langapi/mode.h>
 #include <linking/static_lifetime_init.h>
 
 #include "dfcc_lift_memory_predicates.h"
+#include "dfcc_utils.h"
 
 invalid_function_contract_pair_exceptiont::
   invalid_function_contract_pair_exceptiont(

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h

@@ -14,21 +14,14 @@ Date: February 2023
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
 
-#include <ansi-c/goto-conversion/goto_convert_class.h>
-
+#include <util/expr.h>
 #include <util/message.h>
 #include <util/namespace.h>
-#include <util/std_expr.h>
-
-#include "dfcc_contract_mode.h"
 
-#include <set>
-
-class goto_modelt;
-class message_handlert;
-class dfcc_libraryt;
-class code_with_contract_typet;
 class conditional_target_group_exprt;
+class dfcc_libraryt;
+class goto_modelt;
+class goto_programt;
 
 /// Translates assigns and frees clauses of a function contract or
 /// loop contract into GOTO programs that build write sets or havoc write sets.

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp

@@ -8,24 +8,13 @@ Date: August 2022
 \*******************************************************************/
 #include "dfcc_contract_functions.h"
 
-#include <util/expr_util.h>
-#include <util/fresh_symbol.h>
-#include <util/invariant.h>
 #include <util/mathematical_expr.h>
-#include <util/namespace.h>
-#include <util/pointer_offset_size.h>
-#include <util/std_expr.h>
-
-#include <goto-programs/goto_model.h>
-
-#include <ansi-c/c_expr.h>
-#include <goto-instrument/contracts/utils.h>
-#include <langapi/language_util.h>
+#include <util/symbol.h>
 
 #include "dfcc_contract_clauses_codegen.h"
 #include "dfcc_instrument.h"
-#include "dfcc_library.h"
 #include "dfcc_spec_functions.h"
+#include "dfcc_utils.h"
 
 dfcc_contract_functionst::dfcc_contract_functionst(
   const symbolt &pure_contract_symbol,

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h

@@ -14,24 +14,15 @@ Date: August 2022
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
 
-#include <ansi-c/goto-conversion/goto_convert_class.h>
-
 #include <util/message.h>
 #include <util/namespace.h>
-#include <util/std_expr.h>
-
-#include "dfcc_contract_mode.h"
-
-#include <set>
 
-class goto_modelt;
-class message_handlert;
-class dfcc_libraryt;
+class code_with_contract_typet;
+class dfcc_contract_clauses_codegent;
 class dfcc_instrumentt;
+class dfcc_libraryt;
 class dfcc_spec_functionst;
-class dfcc_contract_clauses_codegent;
-class code_with_contract_typet;
-class conditional_target_group_exprt;
+class goto_modelt;
 
 /// Generates GOTO functions modelling a contract assigns and frees clauses.
 ///

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp

@@ -9,27 +9,12 @@ Date: August 2022
 
 #include "dfcc_contract_handler.h"
 
-#include <util/arith_tools.h>
-#include <util/c_types.h>
-#include <util/expr_util.h>
-#include <util/format_type.h>
-#include <util/fresh_symbol.h>
-#include <util/invariant.h>
-#include <util/mathematical_expr.h>
-#include <util/namespace.h>
-#include <util/pointer_offset_size.h>
-#include <util/std_expr.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_function_pointers.h>
 
-#include <ansi-c/c_expr.h>
-#include <goto-instrument/contracts/utils.h>
 #include <langapi/language_util.h>
 
-#include "dfcc_instrument.h"
-#include "dfcc_library.h"
-#include "dfcc_spec_functions.h"
+#include "dfcc_utils.h"
 #include "dfcc_wrapper_program.h"
 
 std::map<irep_idt, dfcc_contract_functionst>

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h

@@ -13,25 +13,20 @@ Date: August 2022
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_HANDLER_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_HANDLER_H
 
-#include <ansi-c/goto-conversion/goto_convert_class.h>
-
-#include <util/message.h>
-#include <util/namespace.h>
-#include <util/std_expr.h>
-
 #include "dfcc_contract_functions.h"
+#include "dfcc_contract_mode.h"
 
+#include <map>
 #include <set>
 
-class goto_modelt;
-class message_handlert;
-class dfcc_libraryt;
+class code_typet;
+class dfcc_contract_clauses_codegent;
 class dfcc_instrumentt;
+class dfcc_libraryt;
 class dfcc_lift_memory_predicatest;
 class dfcc_spec_functionst;
-class dfcc_contract_clauses_codegent;
-class code_with_contract_typet;
-class conditional_target_group_exprt;
+class goto_modelt;
+class goto_programt;
 
 /// A contract is represented by a function declaration or definition
 /// with contract clauses attached to its signature:

src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp

@@ -7,17 +7,14 @@ Author: Remi Delmas, delmasrd@amazon.com
 \*******************************************************************/
 #include "dfcc_infer_loop_assigns.h"
 
-#include <util/expr.h>
 #include <util/find_symbols.h>
-#include <util/message.h>
 #include <util/pointer_expr.h>
-#include <util/std_code.h>
 
 #include <goto-programs/goto_inline.h>
 
 #include <analyses/goto_rw.h>
+#include <analyses/local_may_alias.h>
 #include <goto-instrument/contracts/utils.h>
-#include <goto-instrument/havoc_utils.h>
 
 #include "dfcc_loop_nesting_graph.h"
 #include "dfcc_root_object.h"

src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h

@@ -12,15 +12,11 @@ Author: Remi Delmas, delmasrd@amazon.com
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INFER_LOOP_ASSIGNS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INFER_LOOP_ASSIGNS_H
 
-#include <analyses/local_may_alias.h>
 #include <goto-instrument/loop_utils.h>
 
-#include "dfcc_loop_nesting_graph.h"
-
-class source_locationt;
-class messaget;
 class namespacet;
 class message_handlert;
+struct dfcc_loop_nesting_graph_nodet;
 
 /// Collect identifiers that are local to `loop`.
 std::unordered_set<irep_idt> gen_loop_locals_set(

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

@@ -13,16 +13,18 @@ Date: April 2023
 #include "dfcc_instrument_loop.h"
 #include <ansi-c/goto-conversion/goto_convert_class.h>
 
-#include <util/format_expr.h>
-#include <util/fresh_symbol.h>
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/expr_util.h>
 
 #include <goto-instrument/contracts/utils.h>
 
 #include "dfcc_cfg_info.h"
 #include "dfcc_contract_clauses_codegen.h"
-#include "dfcc_instrument.h"
+#include "dfcc_library.h"
 #include "dfcc_loop_tags.h"
 #include "dfcc_spec_functions.h"
+#include "dfcc_utils.h"
 
 dfcc_instrument_loopt::dfcc_instrument_loopt(
   goto_modelt &goto_model,