Loop assigns inference does not compute may-alias for `ID_member`.

[qinheping]

CBMC version: current develop (4f660c4)
Operating system: Ubuntu 20.04
Exact command line resulting in the issue:

goto-cc main.c
goto-instrument --apply-loop-contracts a.out a.out
cbmc a.out

What behaviour did you expect:

** 0 of 12 failed (1 iterations)
VERIFICATION SUCCESSFUL

What happened instead:

[main.assigns.4] line 31 Check that t->n is assignable: FAILURE
[main.assigns.6] line 31 Check that t->n is assignable: FAILURE

** 2 of 12 failed (2 iterations)
VERIFICATION FAILED

In the following program,

#include <stdlib.h>

typedef struct node
{
  int h;
  struct node *n;
} *List;

int main()
{
  List t = (List)malloc(sizeof(struct node));
  List end = (List)malloc(sizeof(struct node));
  while(__VERIFIER_nondet_int())
    __CPROVER_loop_invariant(
      __CPROVER_POINTER_OBJECT(t) == __CPROVER_POINTER_OBJECT(end) ||
      __CPROVER_POINTER_OBJECT(t) == __CPROVER_POINTER_OBJECT(__CPROVER_loop_entry(t)))
    {
      t = end;
      t->n = 0;
    }
}

There are assign-left-hand-sides t and t->n. The current loop assigns inference algorithm infer loop assigns (t, t->n). However, the correct loop assigns should be (t, end->n) because t points to the object pointed to end instead of __CPROVER_loop_entry(t) when we access member t->n.

The cause of the problem is the lack of alias analysis to infer assigns target with type ID_member---we now only infer alias for lhs with type ID_dereference.

This issue is also one blocker of the problem in #7595.