Spurious warning Write to unknown address: privatization is unsound. even though no write occurs #765
Description
#include<pthread.h>
#include<assert.h>
int counter = 0;
pthread_mutex_t lock1;
void* producer(void* param) {
pthread_mutex_lock(&lock1);
counter = 0;
pthread_mutex_unlock(&lock1);
}
void* consumer(void* param) {
pthread_mutex_lock(&lock1);
assert(counter >= 0);
pthread_mutex_unlock(&lock1);
}
int main() {
pthread_t thread;
pthread_t thread2;
pthread_create(&thread,NULL,producer,NULL);
pthread_create(&thread2,NULL,consumer,NULL);
}For this innocuous program, Goblint currently produces the following output:
./goblint 5.c --enable dbg.debug --enable dbg.regression
[Info][Unsound] Write to unknown address: privatization is unsound. (5.c:15:5-15:25)
Pruning result
Summary for all memory locations:
safe: 1
vulnerable: 0
unsafe: 0
-------------------
total: 1
The warning [Info][Unsound] Write to unknown address: privatization is unsound. (5.c:15:5-15:25) happening at counter >= 0 is spurious as no actual write access is happening here.