CORE
main.c
--enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check
^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$
^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[(\(.*\))?0\] is assignable: SUCCESS$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
--
^\[.*assigns.*\].*: FAILURE$
--
In f1, the assigns clause specifies `*(p->buf)` as target (which can be invalid)
and assigns `p->buf[0]` unconditionally. When both target and lhs are invalid,
its  inclusion check can be trivially satisfied or not but we expect in all
cases a  null pointer failure and an invalid pointer error to occur 
on the assignment.

In f2 tests this behaviour with chained dereferences.