Uniqueness analysis for Juliet suite std_thread wrappers #186
Description
Would be good to have this sooner rather than later. Goblint can't analyze Juliet suite race detection stuff because they use some wrappers that end up creating pointers to structs containing the mutex. One could obviously just take their lock operations as native, but these are much simpler programs than all the idioms we handle with symbolic locks. It does not seem unreasonable to think that we should be able to analyzer the following.
struct { pthread_mutex_t mutex; } *mylock;
int myglobal;
void *t_fun(void *arg) {
pthread_mutex_lock(&mylock->mutex);
myglobal=myglobal+1;
pthread_mutex_unlock(&mylock->mutex);
return NULL;
}
int main(void) {
pthread_t id;
mylock = malloc(sizeof(*mylock));
pthread_mutex_init(&mylock->mutex, NULL);
pthread_create(&id, NULL, t_fun, NULL);
pthread_mutex_lock(&mylock->mutex);
myglobal=myglobal+1;
pthread_mutex_unlock(&mylock->mutex);
pthread_join (id, NULL);
return 0;
}