dfcc_loop_nesting_grapht: cleanup loop includes

Directly refer to the classes rather than going through a series of
(member) typedefs and one header that is rather unrelated.

Author: tautschnig

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

@@ -522,16 +522,15 @@ dfcc_cfg_infot::dfcc_cfg_infot(
   : function_id(function_id),
     goto_function(goto_function),
     top_level_write_set(top_level_write_set),
-    log(message_handler),
     ns(symbol_table)
 {
   dfcc_loop_nesting_grapht loop_nesting_graph;
   goto_programt &goto_program = goto_function.body;
-  messaget log(message_handler);
   if(loop_contract_mode != dfcc_loop_contract_modet::NONE)
   {
+    messaget log(message_handler);
     dfcc_check_loop_normal_form(goto_program, log);
-    loop_nesting_graph = build_loop_nesting_graph(goto_program, log);
+    loop_nesting_graph = build_loop_nesting_graph(goto_program);
 
     const auto head = check_inner_loops_have_contracts(loop_nesting_graph);
     if(head.has_value())

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

@@ -17,7 +17,6 @@ Date: March 2023
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
 
-#include <util/message.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -33,6 +32,7 @@ Date: March 2023
 class dfcc_utilst;
 class dfcc_libraryt;
 class goto_functiont;
+class message_handlert;
 
 /// \brief Describes a single loop for the purpose of DFCC loop contract
 /// instrumentation.
@@ -297,7 +297,6 @@ class dfcc_cfg_infot
   const irep_idt &function_id;
   goto_functiont &goto_function;
   const exprt &top_level_write_set;
-  messaget log;
   const namespacet ns;
 
   /// True iff \p id is in the valid range for a loop id or is equal to

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

@@ -12,12 +12,12 @@ Date: March 2023
 
 #include "dfcc_loop_nesting_graph.h"
 
-#include <util/invariant.h>
+#include <analyses/natural_loops.h>
 
 dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet(
   const goto_programt::targett &head,
   const goto_programt::targett &latch,
-  const loopt &instructions)
+  const loop_templatet<goto_programt::targett> &instructions)
   : head(head), latch(latch), instructions(instructions)
 {
 }

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

@@ -18,7 +18,7 @@ Date: March 2023
 
 #include <util/graph.h>
 
-#include <goto-instrument/loop_utils.h>
+#include <analyses/loop_analysis.h>
 
 class messaget;
 
@@ -29,7 +29,7 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
   dfcc_loop_nesting_graph_nodet(
     const goto_programt::targett &head,
     const goto_programt::targett &latch,
-    const loopt &instructions);
+    const loop_templatet<goto_programt::targett> &instructions);
 
   /// Loop head instruction
   goto_programt::targett head;
@@ -38,7 +38,7 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
   goto_programt::targett latch;
 
   /// Set of loop instructions
-  loopt instructions;
+  loop_templatet<goto_programt::targett> instructions;
 };
 
 typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;