Skip to content

Commit 670d9fd

Browse files
committed
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.
1 parent 3b7004c commit 670d9fd

File tree

2 files changed

+8
-7
lines changed

2 files changed

+8
-7
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,12 @@ Date: March 2023
1212

1313
#include "dfcc_loop_nesting_graph.h"
1414

15-
#include <util/invariant.h>
15+
#include <analyses/natural_loops.h>
1616

1717
dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet(
1818
const goto_programt::targett &head,
1919
const goto_programt::targett &latch,
20-
const loopt &instructions)
20+
const loop_templatet<goto_programt::targett> &instructions)
2121
: head(head), latch(latch), instructions(instructions)
2222
{
2323
}

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

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ Date: March 2023
1818

1919
#include <util/graph.h>
2020

21-
#include <goto-instrument/loop_utils.h>
21+
#include <analyses/loop_analysis.h>
2222

2323
class messaget;
2424

@@ -29,16 +29,17 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
2929
dfcc_loop_nesting_graph_nodet(
3030
const goto_programt::targett &head,
3131
const goto_programt::targett &latch,
32-
const loopt &instructions);
32+
const loop_templatet<goto_programt::targett> &instructions);
3333

3434
/// Loop head instruction
35-
goto_programt::targett head;
35+
const goto_programt::targett head;
3636

3737
/// Loop latch instruction
38-
goto_programt::targett latch;
38+
const goto_programt::targett latch;
3939

4040
/// Set of loop instructions
41-
loopt instructions;
41+
/// Should be `const`, but this doesn't work with Visual Studio.
42+
loop_templatet<goto_programt::targett> instructions;
4243
};
4344

4445
typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;

0 commit comments

Comments
 (0)