[pulse] Take into account reachable addresses from pre state

[danielmercier]

Pulse emits a false positive on the following cpp example:

struct list_item {
  list_item* next;
};

struct list {
  list_item* first;
  list_item* last;
};

void append(list& l) {
  list_item* new_cell = new list_item;
  new_cell->next = nullptr;

  if (l.last == nullptr) {
    l.first = new_cell;
  } else {
    l.last->next = new_cell;
  }

  l.last = new_cell;
}

void delete_list(list& l) {
  list_item* cell = l.first;
  list_item* next_cell;

  while (cell != nullptr) {
    next_cell = cell->next;
    delete cell;
    cell = next_cell;
  }
}

void leak_false_positive() {
  list l = {nullptr, nullptr};

  append(l);
  append(l);

  delete_list(l);
}

The issue seems to be that when calling append for the second time, both l.first and l.last are pointing to the same value. When instantiating the summary Pulse misses to see that l.first->next and l.last should point to the same value.

The reason seems to be that Pulse is only following what is happening to l.last in the post, but not what is happening to the input value of l.last (which is l.first in the second call to append).

This PR fixes this issue, I also included more examples fixed by this commit.

[facebook-github-bot]

@jvillard has imported this pull request. If you are a Meta employee, you can view this diff on Phabricator.

[jvillard]

Many thanks @danielmercier, great catch!