Exploit malloc uniqueness for assignments of struct members as well

[michael-schwarz]

Since #722, we can detect if heap objects are unique and then do strong updates. We would need the same capability for partial updates of structs for one of the benchmarks I am considering for #970.

It should in principle not be hard to achieve. A possible example program is given by:

// PARAM: --set ana.malloc.unique_address_count 2

#include <stdlib.h>
#include <stdint.h>
#include <goblint.h>

struct s {
  int x;
  int y;
};

int main() {
  struct s *ptr = malloc(sizeof(struct s));
  int p;

  ptr->x = 0;
  ptr->y = 1;

  __goblint_check(ptr->x == 0);
  __goblint_check(ptr->y == 1);

  ptr->x = 1;
  ptr->y = 0;
  __goblint_check(ptr->x == 1);
  __goblint_check(ptr->y == 0);
}

Currently, the second block of asserts is unknown.

[michael-schwarz]

Rolled into #970.

[michael-schwarz]

Closed in #970.