With dbg.full-output off: Combination of ana.malloc.unique_address_count >= 2 &threadid analysis deactivated unsound

[michael-schwarz]

// PARAM: --set ana.malloc.unique_address_count 2 --set ana.activated[-] threadid

typedef struct list {
 struct list *next;
} mlist;

mlist *head;

int insert_list(mlist *l){
  l = (mlist*)malloc(sizeof(mlist));
  l->next = head;

  head = l;
  return 0;
}

int main(void){
  mlist *mylist;
  insert_list(mylist);
  insert_list(mylist);

  while(head!=((void *)0)) {
    head = head->next;
  }

  __goblint_check(1);
}

The analysis claims here that the while loop is never left. Deactivating either option means the analysis succeeds.

[michael-schwarz]

I tried to add --enable dbg.full-output to understand what's going on. Turn out this fixes the problem!

This seems to be some sort of regression of #1312 ?!

[sim642]

That's definitely odd. Are the uniqueness counters looking at the variable name somewhere then?