BUG: Failure at MOCalculator.cpp:65/getStoreOffset()!
bupt01 opened this issue · 2 comments
I tested a C language file prog5.c, and the source code is as follows:
`#include <assert.h>
#include <stdint.h>
#include <stdatomic.h>
#include <pthread.h>
#include<stdlib.h>
pthread_mutex_t lock1;
pthread_mutex_t lock2;
pthread_mutex_t lock3;
void *thread_1(void *arg) {
pthread_mutex_lock(&lock3);
pthread_mutex_lock(&lock1);
pthread_mutex_unlock(&lock1);
pthread_mutex_unlock(&lock3);
return NULL;
}
void *thread_2(void *arg) {
pthread_mutex_lock(&lock2);
pthread_mutex_lock(&lock3);
pthread_mutex_unlock(&lock3);
pthread_mutex_unlock(&lock2);
return NULL;
}
void *thread_3(void *arg) {
pthread_mutex_lock(&lock2); //fix2'
pthread_mutex_lock(&lock1);
pthread_mutex_unlock(&lock1);
pthread_mutex_unlock(&lock2); //fix2'
return NULL;
}
int main(int argc, char const *argv[])
{
pthread_t t[3];
pthread_create(&t[0], NULL, thread_1, NULL);
pthread_create(&t[1], NULL, thread_2, NULL);
pthread_create(&t[2], NULL, thread_3, NULL);
}`
After entering the command: genmc prog5.c -disable-race-detection,The execution result is as follows:
BUG: Failure at MOCalculator.cpp:65/getStoreOffset()!
I would like to ask what the reason is for this.
Thanks for the report.
This seems like a reproduction of #45. I will try to push a fix in the next release.
Should be fixed in v0.10.0.