CORE
main.c
--enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check
^EXIT=10$
^SIGNAL=0$
^\[f1.assigns.\d+\].*line 16 Check that \*p->buf is valid: FAILURE$
^\[f1.assigns.\d+\].*line 18 Check that p->buf\[(\(.*\))?0\] is assignable: FAILURE$
^\[f2.assigns.\d+\].*line 21 Check that \*pp->p->buf is valid: FAILURE$
^\[f2.assigns.\d+\].*line 23 Check that pp->p->buf\[(\(.*\))?0\] is assignable: FAILURE$
^VERIFICATION FAILED$
--
--
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 the target
validity check to fail.

In f2 tests this behaviour with chained dereferences.