Skip to content

Commit

Permalink
Adding move constructors
Browse files Browse the repository at this point in the history
  • Loading branch information
JohnDumbell authored and smowton committed Mar 7, 2019
1 parent eac449d commit 3a23028
Show file tree
Hide file tree
Showing 4 changed files with 53 additions and 0 deletions.
35 changes: 35 additions & 0 deletions src/goto-symex/goto_state.h
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,11 @@ class goto_statet
unsigned remaining_vccs = 0;

/// Constructors
goto_statet() = default;
goto_statet &operator=(const goto_statet &other) = default;
goto_statet &operator=(goto_statet &&other) = default;
goto_statet(const goto_statet &other) = default;

explicit goto_statet(const class goto_symex_statet &s);

goto_statet(
Expand All @@ -69,6 +74,36 @@ class goto_statet
: guard(true_exprt(), guard_manager), source(_source)
{
}

/// Partial-move constructor.
/// This will only move level2, value_set, guard and propagation fields. This
/// will mean that you shouldn't use it as an active state in symex, but you
/// can still look at its statistics and source values.
goto_statet(goto_statet &other, bool partial_move)
: depth(other.depth),
level2(std::move(other.level2)),
value_set(std::move(other.value_set)),
guard(std::move(other.guard)),
source(other.source),
propagation(std::move(other.propagation)),
atomic_section_id(other.atomic_section_id),
total_vccs(other.total_vccs),
remaining_vccs(other.remaining_vccs)
{
}

goto_statet(goto_statet &&other)
: depth(other.depth),
level2(std::move(other.level2)),
value_set(std::move(other.value_set)),
guard(std::move(other.guard)),
source(std::move(other.source)),
propagation(std::move(other.propagation)),
atomic_section_id(other.atomic_section_id),
total_vccs(other.total_vccs),
remaining_vccs(other.remaining_vccs)
{
}
};

#endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H
4 changes: 4 additions & 0 deletions src/goto-symex/renaming_level.h
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,10 @@ struct symex_level2t : public symex_renaming_levelt

symex_level2t() = default;
~symex_level2t() override = default;
symex_level2t &operator=(const symex_level2t &other) = default;
symex_level2t &operator=(symex_level2t &&other) = default;
symex_level2t(const symex_level2t &other) = default;
symex_level2t(symex_level2t &&other) = default;
};

/// Undo all levels of renaming
Expand Down
9 changes: 9 additions & 0 deletions src/goto-symex/symex_target.h
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,15 @@ class symex_targett
pc(_goto_program.instructions.begin())
{
}

sourcet(sourcet &&other) noexcept
: thread_nr(other.thread_nr), function_id(other.function_id), pc(other.pc)
{
}

sourcet(const sourcet &other) = default;
sourcet &operator=(const sourcet &other) = default;
sourcet &operator=(sourcet &&other) = default;
};

enum class assignment_typet
Expand Down
5 changes: 5 additions & 0 deletions src/pointer-analysis/value_set.h
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,11 @@ class value_sett
{
}

value_sett(value_sett &&other)
: location_number(other.location_number), values(std::move(other.values))
{
}

virtual ~value_sett() = default;

value_sett(const value_sett &other) = default;
Expand Down

0 comments on commit 3a23028

Please sign in to comment.