projects
/
model-checker-benchmarks.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Makefiles: use appropriate preprocessor vs. compiler flags
[model-checker-benchmarks.git]
/
ms-queue
/
main.c
diff --git
a/ms-queue/main.c
b/ms-queue/main.c
index c09470de2b22f3760d4b3e2fcb2ee3c3b3e0b195..b541b010c2837d04e798b6db73a2eb4d3dbc4f31 100644
(file)
--- 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 i;
int *param;
unsigned int in_sum = 0, out_sum = 0;
- int zero = 0;
queue = calloc(1, sizeof(*queue));
MODEL_ASSERT(queue);
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++)
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]);
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);
free(param);
free(threads);