From 48ba6af4a6b346152f6f0db23d2fd0a9c5866f46 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 16 Dec 2024 12:08:53 +0200 Subject: [PATCH] Add ex-10 from traces --- .../13-privatized/89-traces-ex-10.c | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 tests/regression/13-privatized/89-traces-ex-10.c diff --git a/tests/regression/13-privatized/89-traces-ex-10.c b/tests/regression/13-privatized/89-traces-ex-10.c new file mode 100644 index 0000000000..4822528eeb --- /dev/null +++ b/tests/regression/13-privatized/89-traces-ex-10.c @@ -0,0 +1,30 @@ +#include +#include + +int g = 7; // matches precise read +pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&A); + pthread_mutex_lock(&B); + g = 42; + pthread_mutex_unlock(&B); + g = 7; + pthread_mutex_unlock(&A); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(&B); + // __goblint_check(g == 7); // UNKNOWN! + pthread_mutex_unlock(&B); + + pthread_mutex_lock(&A); + pthread_mutex_lock(&B); + __goblint_check(g == 7); + return 0; +}