analyzer
analyzer copied to clipboard
Wrong location in `Invalid pointer dereference` warning
For regression tests 28 78 and 28 79 there are warnings:
[Warning][Unknown] lval (& s)->datum points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:129-22:139)
[Warning][Unknown] lval (& s)->mutex points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:129-22:139)
The warning location, line 22 in sv-comp.c is just a macro definition __VERIFIER_nondet(int), and in the tests, (&s->mutex) does not have anything to do with __VERIFIER_nondet(int):
int main () {
pthread_mutex_init(&A.mutex, NULL);
pthread_mutex_init(&B.mutex, NULL);
int x = __VERIFIER_nondet_int();
// struct s *s = malloc(sizeof(struct s));
struct s *s;
//struct q *q;
int *d;
pthread_mutex_t *m;
if (x) {
s = &A;
x++;
} else {
s = &B;
x++;
}
//q = &s->inside;
m = &s->mutex;
d = &s->datum;
create_threads(t);
pthread_mutex_lock(m);
access_or_assert_racefree(*d); // UNKNOWN
pthread_mutex_unlock(m);
join_threads(t);
return 0;
}