deque: re-insert deleted MODEL_ASSERT()

[model-checker-benchmarks.git] / spsc-queue / spsc-queue.cc

diff --git a/spsc-queue/spsc-queue.cc b/spsc-queue/spsc-queue.cc
index ef7b02635d8f1e525d14191b9ba6b85b33fe7ec2..f8528a862acd8f5097ebb3d781e73e8eb7955864 100644 (file)
--- a/spsc-queue/spsc-queue.cc
+++ b/spsc-queue/spsc-queue.cc
@@ -2,27 +2,33 @@
 
 #include "queue.h"
 
-spsc_queue<int> q;
+spsc_queue<int> *q;
 
        void thread(unsigned thread_index)
        {
                if (0 == thread_index)
                {
-                       q.enqueue(11);
+                       q->enqueue(11);
                }
                else
                {
-                       int d = q.dequeue();
+                       int d = q->dequeue();
                        RL_ASSERT(11 == d);
                }
        }
 
-int main()
+int user_main(int argc, char **argv)
 {
        thrd_t A, B;
+
+       q = new spsc_queue<int>();
+
        thrd_create(&A, (thrd_start_t)&thread, (void *)0);
        thrd_create(&B, (thrd_start_t)&thread, (void *)1);
        thrd_join(A);
        thrd_join(B);
+
+       delete q;
+
        return 0;
 }