diff --git a/tests/regression/03-practical/48-symbolic-thread-array-init.c b/tests/regression/03-practical/48-symbolic-thread-array-init.c new file mode 100644 index 0000000000..45d5869215 --- /dev/null +++ b/tests/regression/03-practical/48-symbolic-thread-array-init.c @@ -0,0 +1,36 @@ +// Per-thread array pointers passed via argument but initialized before thread create. +// Extracted from silver searcher. +#include +#include +#include +extern int __VERIFIER_nondet_int(); + +void *thread(void *arg) { + int *p = arg; + int i = *p; // 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)); + int *is = malloc(threads_total * sizeof(int)); + + // create threads + for (int i = 0; i < threads_total; i++) { + is[i] = i; // NORACE + pthread_create(&tids[i], NULL, &thread, &is[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(is); + + return 0; +}