// This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks // // SPDX-FileCopyrightText: 2005-2021 University of Tartu & Technische Universität München // // SPDX-License-Identifier: MIT #include extern void abort(void); void reach_error() { assert(0); } void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } } extern int __VERIFIER_nondet_int(); #include int glob1 = 0; pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; void *t_fun(void *arg) { int t = __VERIFIER_nondet_int(); pthread_mutex_lock(&mutex1); if(t == 42) { glob1 = 1; } t = glob1; __VERIFIER_assert(!(t == 0)); glob1 = 0; pthread_mutex_unlock(&mutex1); return NULL; } int main(void) { pthread_t id; pthread_create(&id, NULL, t_fun, NULL); pthread_mutex_lock(&mutex1); pthread_mutex_unlock(&mutex1); pthread_join (id, NULL); return 0; }