Mutex-Meet unsound (function pointers get lost)

[michael-schwarz]

This is a follow-up to #1557, which is extracted as the issue has nothing to do with relational analysis.

#include<pthread.h>
#include<stdlib.h>
#include<stdio.h>
struct a {
  int (*b)();
};

struct a* t;
int m() {
    printf("m\n");
    int x =5;
}

void* j(void* arg) {};

void munge(struct a** a) {
    struct a r = **a;
    r.b();
}


void main() {
    pthread_t tid;
    pthread_create(&tid, 0, j, NULL);
    t = calloc(1, sizeof(struct a));
    t->b = &m;
    munge(&t);
}

For this program, Goblint with the mutex-meet privatization for base determines m to be uncalled which does not hold in the concrete.

We, however do produce a warning:

[Warning][Imprecise][Call] Function pointer *(r.b) may contain unknown functions. (2.c:18:5-18:10)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (2.c:18:5-18:10)

[michael-schwarz]

The example can be further simplified to

#include<pthread.h>
#include<stdlib.h>
#include<stdio.h>
struct a {
  void (*b)();
};

struct a* t;
void m() {
    printf("m\n");
}

void* j(void* arg) {};

void main() {
    pthread_t tid;
    pthread_create(&tid, 0, j, NULL);
    t = calloc(1, sizeof(struct a));
    t->b = &m;
    struct a r = *t;
    r.b();
}

[michael-schwarz]

Closed by #1559.