Apron: Both branches dead after malloc

[michael-schwarz]

In the epic saga of problems with both branches being dead in the relational analysis, we proudly present the next example:

// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet --sets ana.apron.domain interval
// Checks that assinging to malloc'ed memory does not cause both branches to be dead
#include <pthread.h>

void nop(void* arg) {
}

void main() {
  pthread_t thread;
  pthread_create(&thread, 0, &nop, 0);

  long *k = malloc(sizeof(long));
  *k = 5;
  if (1)
    ;
}

[sim642]

Isn't this also an issue for base's mutex-meet?

[michael-schwarz]

It would seem like it should be, but it works without any issues for base.

[sim642]

I guess base's existing logic for turning bottoms into tops is somehow covering this already.