Spurious null-pointer failure on self-referential data structure

[xaaronc]

CBMC version: 5.24.0 (cbmc-5.24.0-31-ge989d743f)
Operating system: macOS
Exact command line resulting in the issue: cbmc/src/cbmc/cbmc --pointer-check --trace --stop-on-fail test.c
What behaviour did you expect: verification successful
What happened instead: verification failure

Given the following test.c:

#include <stdlib.h>

struct A { struct A *p; };

struct A *f(struct A **y) {
    return (*y)->p = NULL;
}

int main(void) {
    struct A x = { &x };
    f(&x.p);
}

I get a verification failure with the following counterexample:

State 28 file test.c function main line 13 thread 0
----------------------------------------------------
  y=&x!0@1.p (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 29 file test.c function f line 7 thread 0
----------------------------------------------------
  x.p=((struct A *)NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

Violated property:
  file test.c function f line 7 thread 0
  dereference failure: pointer NULL in (*y)->p
  !(POINTER_OBJECT(*y) == POINTER_OBJECT(((struct A **)NULL)))

I would expect this not to fail, even though f modifies the pointer it is dereferencing, since C11 specifies (§6.5.16) that the value computation of the LHS and RHS of the assignment is sequenced before the update.

Curiously, if I change the body of f to:

    (*y)->p = NULL;
    return NULL;

CBMC is happy.

[tautschnig]

Thank you for reporting this issue, and also for the very nice reproducer. The issue should be addressed by #5858 (once merged).