Skip to content

Commit 35db01f

Browse files
committed
Delete copy construction of class java_bytecode_parse_treet.
This deletes the default copy constructors of `java_bytecode_parse_treet`, but allows move construction. This enforces allowing move semantics only and prevents accidental copying.
1 parent 1676928 commit 35db01f

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,14 @@ Author: Daniel Kroening, [email protected]
2222
class java_bytecode_parse_treet
2323
{
2424
public:
25+
// Disallow copy construction and copy assignment, but allow move construction
26+
// and move assignment.
27+
java_bytecode_parse_treet(const java_bytecode_parse_treet &) = delete;
28+
java_bytecode_parse_treet &
29+
operator=(const java_bytecode_parse_treet &) = delete;
30+
java_bytecode_parse_treet(java_bytecode_parse_treet &&) = default;
31+
java_bytecode_parse_treet &operator=(java_bytecode_parse_treet &&) = default;
32+
2533
virtual ~java_bytecode_parse_treet() = default;
2634
class annotationt
2735
{

0 commit comments

Comments
 (0)