Our model-checker doesn't support constructors which perform
model-checking actions (e.g, atomic initialization) at load time (e.g.,
in a static execution of the constructor), since this happens before the
model-check object is created. Maybe we'll fix that in the future, but
for now, don't construct the queue at load time.
void thread(unsigned thread_index)
{
if (0 == thread_index)
{
void thread(unsigned thread_index)
{
if (0 == thread_index)
{
int user_main(int argc, char **argv)
{
thrd_t A, B;
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);
thrd_create(&A, (thrd_start_t)&thread, (void *)0);
thrd_create(&B, (thrd_start_t)&thread, (void *)1);
thrd_join(A);
thrd_join(B);