Skip to content

Commit c1938dc

Browse files
committed
Remove unnecessary copy and loss of state information
This commit removes an inline constructor that performed a copy of the state and thus could cause state information to be lost.
1 parent 4cc9611 commit c1938dc

File tree

2 files changed

+4
-13
lines changed

2 files changed

+4
-13
lines changed

src/goto-symex/goto_state.h

+4-2
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,10 @@ Author: Romain Brenguier, [email protected]
2020

2121
#include "renaming_level.h"
2222

23+
// Forward declaration required since subclass is used explicitly
24+
// by the parent class.
25+
class goto_symex_statet;
26+
2327
/// Container for data that varies per program point, e.g. the constant
2428
/// propagator state, when state needs to branch. This is copied out of
2529
/// goto_symex_statet at a control-flow fork and then back into it at a
@@ -83,8 +87,6 @@ class goto_statet
8387
goto_statet(const goto_statet &other) = default;
8488
goto_statet(goto_statet &&other) = default;
8589

86-
explicit goto_statet(const class goto_symex_statet &s);
87-
8890
explicit goto_statet(guard_managert &guard_manager)
8991
: guard(true_exprt(), guard_manager), reachable(true)
9092
{

src/goto-symex/goto_symex_state.h

-11
Original file line numberDiff line numberDiff line change
@@ -272,15 +272,4 @@ class goto_symex_statet final : public goto_statet
272272
goto_symex_statet(const goto_symex_statet &other) = default;
273273
};
274274

275-
inline goto_statet::goto_statet(const class goto_symex_statet &s)
276-
: depth(s.depth),
277-
level2(s.level2),
278-
value_set(s.value_set),
279-
guard(s.guard),
280-
reachable(s.reachable),
281-
propagation(s.propagation),
282-
atomic_section_id(s.atomic_section_id)
283-
{
284-
}
285-
286275
#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H

0 commit comments

Comments
 (0)