From a24dbc352711344468b4724333347cda52c491a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Sep 2013 08:31:31 -0700
Subject: [PATCH] test(buffer): add tests for improving coverage

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/buffer.cpp | 28 +++++++++++++++++++++++-----
 src/util/buffer.h         |  6 +++++-
 2 files changed, 28 insertions(+), 6 deletions(-)

diff --git a/src/tests/util/buffer.cpp b/src/tests/util/buffer.cpp
index 6fc3a65ce..71caa5d41 100644
--- a/src/tests/util/buffer.cpp
+++ b/src/tests/util/buffer.cpp
@@ -20,14 +20,32 @@ static void loop(int n) {
         loop<C>(n-1);
 }
 
-void perftest() {
-    for (unsigned i = 0; i < 10000; i++)
-        loop<buffer<int>>(10000);
-//    for (unsigned i = 0; i < 10000; i++)
-//        loop<std::vector<int>>(10000);
+static void tst1() {
+    buffer<int> b1;
+    buffer<int> b2;
+    b1.push_back(10);
+    lean_assert(b1 != b2);
+    b2.push_back(20);
+    lean_assert(b1 != b2);
+    b2.pop_back();
+    b2.push_back(10);
+    lean_assert(b1 == b2);
+    b2.push_back(20);
+    b2.push_back(20);
+    lean_assert(b1 != b2);
+    b2.shrink(1);
+    lean_assert(b1 == b2);
+    b2.push_back(100);
+    lean_assert(b1 != b2);
+    b2 = b1;
+    lean_assert(b1 == b2);
+    buffer<int> b3(b1);
+    lean_assert(b3 == b1);
+    lean_assert(b1.back() == 10);
 }
 
 int main() {
     loop<buffer<int>>(100);
+    tst1();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/buffer.h b/src/util/buffer.h
index 6f3003ad8..1ef4537e4 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -73,7 +73,7 @@ public:
         return *this;
     }
 
-    bool operator==(buffer const & other) {
+    bool operator==(buffer const & other) const {
         if (size() != other.size()) {
             return false;
         } else {
@@ -85,6 +85,10 @@ public:
         }
     }
 
+    bool operator!=(buffer const & other) const {
+        return !operator==(other);
+    }
+
     T const & back() const { lean_assert(!empty() && m_pos > 0); return m_buffer[m_pos - 1]; }
     T & back() { lean_assert(!empty() && m_pos > 0); return m_buffer[m_pos - 1]; }
     T & operator[](unsigned idx) { lean_assert(idx < size());  return m_buffer[idx]; }