Skip to content

Commit e1a7eb3

Browse files
JohnDumbellsmowton
authored andcommitted
Adding move constructors
1 parent a57d53c commit e1a7eb3

File tree

4 files changed

+53
-0
lines changed

4 files changed

+53
-0
lines changed

src/goto-symex/goto_state.h

+35
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,11 @@ class goto_statet
6161
unsigned remaining_vccs = 0;
6262

6363
/// Constructors
64+
goto_statet() = default;
65+
goto_statet &operator=(const goto_statet &other) = default;
66+
goto_statet &operator=(goto_statet &&other) = default;
67+
goto_statet(const goto_statet &other) = default;
68+
6469
explicit goto_statet(const class goto_symex_statet &s);
6570

6671
goto_statet(
@@ -69,6 +74,36 @@ class goto_statet
6974
: guard(true_exprt(), guard_manager), source(_source)
7075
{
7176
}
77+
78+
/// Partial-move constructor.
79+
/// This will only move level2, value_set, guard and propagation fields. This
80+
/// will mean that you shouldn't use it as an active state in symex, but you
81+
/// can still look at its statistics and source values.
82+
goto_statet(goto_statet &other, bool partial_move)
83+
: depth(other.depth),
84+
level2(std::move(other.level2)),
85+
value_set(std::move(other.value_set)),
86+
guard(std::move(other.guard)),
87+
source(other.source),
88+
propagation(std::move(other.propagation)),
89+
atomic_section_id(other.atomic_section_id),
90+
total_vccs(other.total_vccs),
91+
remaining_vccs(other.remaining_vccs)
92+
{
93+
}
94+
95+
goto_statet(goto_statet &&other)
96+
: depth(other.depth),
97+
level2(std::move(other.level2)),
98+
value_set(std::move(other.value_set)),
99+
guard(std::move(other.guard)),
100+
source(std::move(other.source)),
101+
propagation(std::move(other.propagation)),
102+
atomic_section_id(other.atomic_section_id),
103+
total_vccs(other.total_vccs),
104+
remaining_vccs(other.remaining_vccs)
105+
{
106+
}
72107
};
73108

74109
#endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H

src/goto-symex/renaming_level.h

+4
Original file line numberDiff line numberDiff line change
@@ -125,6 +125,10 @@ struct symex_level2t : public symex_renaming_levelt
125125

126126
symex_level2t() = default;
127127
~symex_level2t() override = default;
128+
symex_level2t &operator=(const symex_level2t &other) = default;
129+
symex_level2t &operator=(symex_level2t &&other) = default;
130+
symex_level2t(const symex_level2t &other) = default;
131+
symex_level2t(symex_level2t &&other) = default;
128132
};
129133

130134
/// Undo all levels of renaming

src/goto-symex/symex_target.h

+9
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,15 @@ class symex_targett
5353
pc(_goto_program.instructions.begin())
5454
{
5555
}
56+
57+
sourcet(sourcet &&other) noexcept
58+
: thread_nr(other.thread_nr), function_id(other.function_id), pc(other.pc)
59+
{
60+
}
61+
62+
sourcet(const sourcet &other) = default;
63+
sourcet &operator=(const sourcet &other) = default;
64+
sourcet &operator=(sourcet &&other) = default;
5665
};
5766

5867
enum class assignment_typet

src/pointer-analysis/value_set.h

+5
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,11 @@ class value_sett
4545
{
4646
}
4747

48+
value_sett(value_sett &&other)
49+
: location_number(other.location_number), values(std::move(other.values))
50+
{
51+
}
52+
4853
virtual ~value_sett() = default;
4954

5055
value_sett(const value_sett &other) = default;

0 commit comments

Comments
 (0)