From: Brian Norris <banorris@uci.edu>
Date: Fri, 8 Mar 2013 23:06:06 +0000 (-0800)
Subject: ms-queue: we should never dequeue 0
X-Git-Tag: oopsla2013-final~17
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=84452c7e91fa7f30f5ff80695d92816b5d209e38

ms-queue: we should never dequeue 0

The test driver is written so that we should never dequeue 0.
---

diff --git a/ms-queue/main.c b/ms-queue/main.c
index c09470d..b541b01 100644
--- a/ms-queue/main.c
+++ b/ms-queue/main.c
@@ -44,7 +44,6 @@ int user_main(int argc, char **argv)
 	int i;
 	int *param;
 	unsigned int in_sum = 0, out_sum = 0;
-	int zero = 0;
 
 	queue = calloc(1, sizeof(*queue));
 	MODEL_ASSERT(queue);
@@ -69,12 +68,9 @@ int user_main(int argc, char **argv)
 	}
 	for (i = 0; i < num_threads; i++)
 		printf("input[%d] = %u\n", i, input[i]);
-	for (i = 0; i < num_threads; i++) {
-		if (output[i] == 0)
-			zero = 1; /* A zero result means queue was empty */
+	for (i = 0; i < num_threads; i++)
 		printf("output[%d] = %u\n", i, output[i]);
-	}
-	MODEL_ASSERT(in_sum == out_sum || zero);
+	MODEL_ASSERT(in_sum == out_sum);
 
 	free(param);
 	free(threads);