From 3d52feadb4282053fbfc5b3d1dbe00f1c8ad7815 Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Wed, 3 Apr 2019 16:02:43 +0100
Subject: Add move assignment operator and move construct for `ref` class.

---
 include/klee/util/Ref.h | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

(limited to 'include')

diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index f6d66d16..4dafdf8e 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -123,6 +123,14 @@ public:
     inc();
   }
 
+  // normal move constructor: invoke the move assignment operator
+  ref(ref<T> &&r) noexcept : ptr(nullptr) { *this = std::move(r); }
+
+  // conversion move constructors: invoke the move assignment operator
+  template <class U> ref(ref<U> &&r) noexcept : ptr(nullptr) {
+    *this = std::move(r);
+  }
+
   // pointer operations
   T *get () const {
     return ptr;
@@ -171,6 +179,35 @@ public:
     return *this;
   }
 
+  // Move assignment operator
+  ref<T> &operator=(ref<T> &&r) noexcept {
+    if (this == &r)
+      return *this;
+    dec();
+    ptr = r.ptr;
+    r.ptr = nullptr;
+    return *this;
+  }
+
+  // Move assignment operator
+  template <class U> ref<T> &operator=(ref<U> &&r) noexcept {
+    if (static_cast<void *>(this) == static_cast<void *>(&r))
+      return *this;
+
+    // Do not swap as the types might be not compatible
+    // Decrement local counter to not hold reference anymore
+    dec();
+
+    // Assign to this ref
+    ptr = cast_or_null<T>(r.ptr);
+
+    // Invalidate old ptr
+    r.ptr = nullptr;
+
+    // Return this pointer
+    return *this;
+  }
+
   T& operator*() const {
     return *ptr;
   }
-- 
cgit 1.4.1