Skip to content

Commit b96bbeb

Browse files
committed
build_loop_nesting_graph: remove unused logging parameter
There is no actual logging done.
1 parent 62fbfe8 commit b96bbeb

File tree

2 files changed

+3
-5
lines changed

2 files changed

+3
-5
lines changed

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ Date: March 2023
1313
#include "dfcc_loop_nesting_graph.h"
1414

1515
#include <util/invariant.h>
16-
#include <util/message.h>
1716

1817
dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet(
1918
const goto_programt::targett &head,
@@ -24,8 +23,7 @@ dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet(
2423
}
2524

2625
/// \pre Loop normal form properties must hold.
27-
dfcc_loop_nesting_grapht
28-
build_loop_nesting_graph(goto_programt &goto_program, messaget &log)
26+
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
2927
{
3028
natural_loops_mutablet natural_loops(goto_program);
3129
dfcc_loop_nesting_grapht loop_nesting_graph;

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,6 @@ typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;
4747
/// loops in the given \p goto_program.
4848
/// A loop is considered nested in an outer loop if its head and its latch are
4949
/// both found in the instructions of the outer loop.
50-
dfcc_loop_nesting_grapht
51-
build_loop_nesting_graph(goto_programt &goto_program, messaget &log);
50+
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program);
51+
5252
#endif

0 commit comments

Comments
 (0)