From 9098aabd488f21b53c83aa64c4f548465c2b43b4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Jul 2025 11:53:22 +0000
Subject: [PATCH] Contracts instrumentation: cleanup unnecessary includes

Reduce includes in header files to a minimum and avoid including what
isn't required. (It seems that IWYU did not catch these.)
---
 src/goto-instrument/contracts/contracts.cpp   | 10 -------
 .../contracts/dynamic-frames/dfcc.cpp         | 23 +---------------
 .../dfcc_contract_clauses_codegen.h           | 15 +++--------
 .../dfcc_contract_functions.cpp               | 15 ++---------
 .../dynamic-frames/dfcc_contract_functions.h  | 17 +++---------
 .../dynamic-frames/dfcc_contract_handler.cpp  | 17 +-----------
 .../dynamic-frames/dfcc_contract_handler.h    | 19 +++++--------
 .../dfcc_infer_loop_assigns.cpp               |  5 +---
 .../dynamic-frames/dfcc_infer_loop_assigns.h  |  6 +----
 .../dynamic-frames/dfcc_instrument_loop.cpp   |  8 +++---
 .../contracts/dynamic-frames/dfcc_library.h   |  1 -
 .../dfcc_lift_memory_predicates.h             |  1 -
 .../dynamic-frames/dfcc_spec_functions.cpp    |  7 ++---
 .../dynamic-frames/dfcc_spec_functions.h      | 16 +++--------
 .../dynamic-frames/dfcc_swap_and_wrap.cpp     | 27 +++----------------
 .../dynamic-frames/dfcc_swap_and_wrap.h       | 20 +++++++-------
 .../contracts/dynamic-frames/dfcc_utils.h     |  3 +--
 .../dynamic-frames/dfcc_wrapper_program.h     | 10 +++----
 src/goto-instrument/contracts/utils.h         |  2 --
 19 files changed, 51 insertions(+), 171 deletions(-)

diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 8cb69c96ed8..7a436300f1d 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/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"
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp
index 0693eef02da..cbc616f7aa9 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp
+++ b/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(
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h
index e78b59b660e..e3db30d054c 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h
+++ b/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.
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp
index d8bb7834432..d57da7795a1 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp
+++ b/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,
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h
index 9a407761388..f3702ddfc6d 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h
+++ b/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.
 ///
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp
index 245f45bcfb3..88e708417e1 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp
+++ b/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>
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h
index 40a1e4ef70a..46b9e04b468 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h
+++ b/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:
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
index 36c724498e2..36a592ff972 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
+++ b/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"
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h
index 8433cf9e705..955213b8ef2 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h
+++ b/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(
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
index 08d7a497a1c..881d16ddcb1 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
+++ b/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,
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
index d119fc1926b..a103da404a5 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
@@ -12,7 +12,6 @@ Author: Remi Delmas, delmasrd@amazon.com
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIBRARY_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIBRARY_H
 
-#include <util/irep.h>
 #include <util/message.h>
 
 #include <goto-programs/goto_instruction_code.h>
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h
index 7b59b2c16d1..848d5aaf600 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.h
@@ -30,7 +30,6 @@ class dfcc_libraryt;
 class dfcc_instrumentt;
 class message_handlert;
 class goto_modelt;
-class exprt;
 class replace_symbolt;
 
 class dfcc_lift_memory_predicatest
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
index 265a99ad924..560a148bb3a 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp
@@ -7,16 +7,17 @@ Author: Remi Delmas, delmarsd@amazon.com
 \*******************************************************************/
 
 #include "dfcc_spec_functions.h"
-#include <ansi-c/goto-conversion/goto_convert_class.h>
 
-#include <util/format_expr.h>
-#include <util/namespace.h>
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/std_code.h>
 
 #include <goto-programs/goto_model.h>
 
 #include <langapi/language_util.h>
 
 #include "dfcc_library.h"
+#include "dfcc_utils.h"
 
 dfcc_spec_functionst::dfcc_spec_functionst(
   goto_modelt &goto_model,
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h
index 5b3b1e7ee11..2f64f551275 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h
@@ -15,22 +15,14 @@ Author: Remi Delmas, delmasrd@amazon.com
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SPEC_FUNCTIONS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SPEC_FUNCTIONS_H
 
-#include <util/arith_tools.h>
-#include <util/c_types.h>
 #include <util/message.h>
-#include <util/std_expr.h>
-#include <util/std_types.h>
-
-#include "dfcc_library.h"
-#include "dfcc_utils.h"
-
-#include <map>
-#include <set>
+#include <util/namespace.h>
 
+class conditional_target_group_exprt;
+class dfcc_libraryt;
 class goto_modelt;
-class message_handlert;
+class goto_programt;
 class symbolt;
-class conditional_target_group_exprt;
 
 /// \brief Represents the different ways to havoc pointers.
 ///
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp
index f74490d3c11..2f57751f7dd 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp
@@ -8,31 +8,12 @@ Author: Remi Delmas, delmarsd@amazon.com
 
 #include "dfcc_swap_and_wrap.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/std_expr.h>
-
-#include <goto-programs/goto_functions.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/goto_model.h>
-#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/remove_skip.h>
 
-#include <ansi-c/c_expr.h>
-#include <ansi-c/cprover_library.h>
-#include <ansi-c/goto-conversion/link_to_library.h>
-#include <goto-instrument/contracts/cfg_info.h>
-#include <goto-instrument/contracts/utils.h>
-#include <linking/static_lifetime_init.h>
+#include "dfcc_contract_handler.h"
+#include "dfcc_instrument.h"
+#include "dfcc_library.h"
+#include "dfcc_utils.h"
 
 dfcc_swap_and_wrapt::dfcc_swap_and_wrapt(
   goto_modelt &goto_model,
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h
index 9fb11f4c171..73c2e909ae3 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h
@@ -16,27 +16,25 @@ Author: Remi Delmas, delmasrd@amazon.com
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
 
-#include <util/arith_tools.h>
-#include <util/c_types.h>
 #include <util/message.h>
-#include <util/std_expr.h>
-#include <util/std_types.h>
+#include <util/namespace.h>
 
-#include <ansi-c/goto-conversion/goto_convert_functions.h>
+#include <goto-instrument/contracts/loop_contract_config.h>
 
-#include "dfcc_contract_handler.h"
-#include "dfcc_instrument.h"
-#include "dfcc_library.h"
-#include "dfcc_spec_functions.h"
+#include "dfcc_contract_mode.h"
 
 #include <map>
 #include <set>
 
+class conditional_target_group_exprt;
+class dfcc_contract_handlert;
+class dfcc_instrumentt;
+class dfcc_libraryt;
+class dfcc_spec_functionst;
 class goto_modelt;
-class messaget;
 class message_handlert;
+class messaget;
 class symbolt;
-class conditional_target_group_exprt;
 
 class dfcc_swap_and_wrapt
 {
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h
index f7f57896123..341371cddef 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h
@@ -13,8 +13,6 @@ Date: August 2022
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_UTILS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_UTILS_H
 
-#include <util/message.h>
-#include <util/namespace.h>
 #include <util/std_expr.h>
 
 #include <set>
@@ -22,6 +20,7 @@ Date: August 2022
 class goto_modelt;
 class goto_programt;
 class message_handlert;
+class symbol_table_baset;
 class symbolt;
 
 struct dfcc_utilst
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
index cd6910507d0..09a0a4e6a81 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
@@ -17,21 +17,17 @@ Author: Remi Delmas, delmasrd@amazon.com
 
 #include <util/message.h>
 #include <util/namespace.h>
-#include <util/std_expr.h>
 
-#include "dfcc_contract_functions.h"
 #include "dfcc_contract_mode.h"
 
 #include <set>
 
-class goto_modelt;
-class messaget;
-class message_handlert;
+class code_with_contract_typet;
+class dfcc_contract_functionst;
 class dfcc_instrumentt;
 class dfcc_libraryt;
 class dfcc_lift_memory_predicatest;
-class code_with_contract_typet;
-class conditional_target_group_exprt;
+class goto_modelt;
 
 /// \brief Generates the body of a wrapper function from a contract
 /// specified using requires, assigns, frees, ensures,
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
index b46f9831cc4..2b81b81c27c 100644
--- a/src/goto-instrument/contracts/utils.h
+++ b/src/goto-instrument/contracts/utils.h
@@ -13,10 +13,8 @@ Date: September 2021
 
 #include <ansi-c/goto-conversion/goto_convert_class.h>
 
-#include <goto-programs/goto_model.h>
 #include <goto-programs/loop_ids.h>
 
-#include <analyses/local_may_alias.h>
 #include <goto-instrument/havoc_utils.h>
 #include <goto-instrument/loop_utils.h>