File tree Expand file tree Collapse file tree 2 files changed +3
-5
lines changed
src/goto-instrument/contracts/dynamic-frames Expand file tree Collapse file tree 2 files changed +3
-5
lines changed Original file line number Diff line number Diff 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
1817dfcc_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;
Original file line number Diff line number Diff 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
You can’t perform that action at this time.
0 commit comments