File tree 2 files changed +7
-7
lines changed
src/goto-instrument/contracts/dynamic-frames 2 files changed +7
-7
lines changed Original file line number Diff line number Diff line change @@ -12,12 +12,12 @@ Date: March 2023
12
12
13
13
#include " dfcc_loop_nesting_graph.h"
14
14
15
- #include < util/invariant .h>
15
+ #include < analyses/natural_loops .h>
16
16
17
17
dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet (
18
18
const goto_programt::targett &head,
19
19
const goto_programt::targett &latch,
20
- const loopt &instructions)
20
+ const loop_templatet<goto_programt::targett> &instructions)
21
21
: head(head), latch(latch), instructions(instructions)
22
22
{
23
23
}
Original file line number Diff line number Diff line change @@ -18,7 +18,7 @@ Date: March 2023
18
18
19
19
#include < util/graph.h>
20
20
21
- #include < goto-instrument/loop_utils .h>
21
+ #include < analyses/loop_analysis .h>
22
22
23
23
class messaget ;
24
24
@@ -29,16 +29,16 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
29
29
dfcc_loop_nesting_graph_nodet (
30
30
const goto_programt::targett &head,
31
31
const goto_programt::targett &latch,
32
- const loopt &instructions);
32
+ const loop_templatet<goto_programt::targett> &instructions);
33
33
34
34
// / Loop head instruction
35
- goto_programt::targett head;
35
+ const goto_programt::targett head;
36
36
37
37
// / Loop latch instruction
38
- goto_programt::targett latch;
38
+ const goto_programt::targett latch;
39
39
40
40
// / Set of loop instructions
41
- loopt instructions;
41
+ const loop_templatet<goto_programt::targett> instructions;
42
42
};
43
43
44
44
typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;
You can’t perform that action at this time.
0 commit comments