From f143811297a0beadf399800a603ae61ac6f29a96 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 20 Sep 2023 14:57:30 +0300
Subject: [PATCH] Extract symbolic-thread-struct-in-array example from
 ProcDump-for-Linux

---
 .../43-symbolic-thread-struct-in-array.c      | 39 +++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 tests/regression/03-practical/43-symbolic-thread-struct-in-array.c

diff --git a/tests/regression/03-practical/43-symbolic-thread-struct-in-array.c b/tests/regression/03-practical/43-symbolic-thread-struct-in-array.c
new file mode 100644
index 0000000000..5039639d0e
--- /dev/null
+++ b/tests/regression/03-practical/43-symbolic-thread-struct-in-array.c
@@ -0,0 +1,39 @@
+// Per-thread structs in array passed via argument.
+// Extracted from concrat/ProcDump-for-Linux.
+#include <stdlib.h>
+#include <pthread.h>
+#include <goblint.h>
+extern int __VERIFIER_nondet_int();
+
+struct thread {
+  int data;
+};
+
+void *thread(void *arg) {
+  struct thread *t = arg;
+  t->data = __VERIFIER_nondet_int(); // NORACE
+  return NULL;
+}
+
+int main() {
+  int threads_total = __VERIFIER_nondet_int();
+  __goblint_assume(threads_total >= 0);
+
+  pthread_t *tids = malloc(threads_total * sizeof(pthread_t));
+  struct thread *ts = malloc(threads_total * sizeof(struct thread));
+
+  // create threads
+  for (int i = 0; i < threads_total; i++) {
+    pthread_create(&tids[i], NULL, &thread, &ts[i]); // may fail but doesn't matter
+  }
+
+  // join threads
+  for (int i = 0; i < threads_total; i++) {
+    pthread_join(tids[i], NULL);
+  }
+
+  free(tids);
+  free(ts);
+
+  return 0;
+}