Merge pull request #109 from vprover/no_leaks_from_options

No leaks from the Options module

Indexing/SubstitutionTree_FastGen.cpp

@@ -104,6 +104,8 @@ class SubstitutionTree::GenMatcher
   ArrayMap<TermList>* _bindings;
 };
 
+const unsigned SubstitutionTree::GenMatcher::BACKTRACK_SEPARATOR;
+
 /**
  * Binding structure to be passed to the @b MatchingUtils::matchArgs
  * method.

Kernel/Problem.cpp

@@ -88,6 +88,8 @@ Problem::~Problem()
   if(_property) { delete _property; }
 
   //TODO: decrease reference counter of clauses (but make sure there's no segfault...)
+
+  UnitList::destroy(_units);
 }
 
 /**

Lib/Stack.hpp

@@ -108,6 +108,15 @@ class Stack
     loadFromIterator(BottomFirstIterator(const_cast<Stack&>(s)));
   }
 
+  Stack(Stack&& s) noexcept
+  {
+    CALL("Stack::Stack(Stack&& s)");
+
+    _capacity = 0;
+    _stack = _cursor = _end = nullptr;
+
+    std::swap(*this,s);
+  }
 
   /** De-allocate the stack
    * @since 13/01/2008 Manchester
@@ -135,11 +144,22 @@ class Stack
   {
     CALL("Stack::operator=");
 
+    if(&s == this) {
+      return *this;
+    }
     reset();
     loadFromIterator(BottomFirstIterator(const_cast<Stack&>(s)));
     return *this;
   }
 
+  Stack& operator=(Stack&& s) noexcept
+  {
+    CALL("Stack::operator=&&");
+
+    std::swap(*this,s);
+    return *this;
+  }
+
 
   /**
    * Put all elements of an iterator onto the stack.
@@ -246,7 +266,7 @@ class Stack
    * @since 11/03/2006 Bellevue
    */
   inline
-  void push(C elem)
+  void push(const C& elem)
   {
     CALL("Stack::push");
 
@@ -258,6 +278,20 @@ class Stack
     _cursor++;
   } // Stack::push()
 
+  inline
+  void push(C&& elem)
+  {
+    CALL("Stack::push");
+
+    if (_cursor == _end) {
+      expand();
+    }
+    ASS(_cursor < _end);
+    new(_cursor) C(std::move(elem));
+    _cursor++;
+  } // Stack::push()
+
+
   /**
    * Pop the stack and return the popped element.
    * @since 11/03/2006 Bellevue
@@ -677,8 +711,8 @@ class Stack
     C* newStack = static_cast<C*>(mem);
     if(_capacity) {
       for (size_t i = 0; i<_capacity; i++) {
-	new(newStack+i) C(_stack[i]);
-	_stack[i].~C();
+        new(newStack+i) C(std::move(_stack[i]));
+        _stack[i].~C();
       }
       // deallocate the old stack
       DEALLOC_KNOWN(_stack,_capacity*sizeof(C),className());
@@ -732,7 +766,7 @@ struct Relocator<Stack<C> >
       Stack<C>* newStack=new(newAddr) Stack<C>( sz );
 
       for(size_t i=0;i<sz;i++) {
-	newStack->push((*oldStack)[i]);
+        newStack->push(std::move((*oldStack)[i]));
       }
 
       oldStack->~Stack<C>();