Value sets and constant propagation are our only sources of points-to
information when resolving dereferences in goto-symex. Therefore,
assuming or branching on equalities of pointer-typed variables must have
us consider both of their value sets to be equal. Else we may end up
with spurious counterexamples as seen with the enclosed regression test
(where we previously did not have any known value for `a`).

Fixes: diffblue#8492

Previously, when a function under proof would assume a pointer to
a structure, the verification harness would construct an instance
of that structure on the stack and pass its address.

This approach is unsound, because it adds to the contractual assumptions
of the function the specifics of the function invocation in the test
harness. For example, a missing bounds constraint in the spec might
go undetected just because the stack-allocated variable happens to
satisfy it.

The most robust way to deal with this, so it seems, is to minimize
the harnesses to merely pass uninitialized variables of the right type
to the function under proof. In particular, where a pointer is expected,
pass an uninitialized pointer, rather than the address of a stack allocated
structure.

Also, remove redundant `x != NULL` preconditions when `IS_FRESH(x,...)`
is assumed. This is not only redundant, but also error prone because of
diffblue/cbmc#8492.

This commit implements those changes for all harnesses implemented so far.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Previously, when a function under proof would assume a pointer to
a structure, the verification harness would construct an instance
of that structure on the stack and pass its address.

This approach is unsound, because it adds to the contractual assumptions
of the function the specifics of the function invocation in the test
harness. For example, a missing bounds constraint in the spec might
go undetected just because the stack-allocated variable happens to
satisfy it.

The most robust way to deal with this, so it seems, is to minimize
the harnesses to merely pass uninitialized variables of the right type
to the function under proof. In particular, where a pointer is expected,
pass an uninitialized pointer, rather than the address of a stack allocated
structure.

Also, remove redundant `x != NULL` preconditions when `IS_FRESH(x,...)`
is assumed. This is not only redundant, but also error prone because of
diffblue/cbmc#8492.

This commit implements those changes for all harnesses implemented so far.

As it turns out, a few specs were incorrect because of missing IS_FRESH
annotations, hidden by the correct allocation in the harness.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Value sets and constant propagation are our only sources of points-to
information when resolving dereferences in goto-symex. Therefore,
assuming or branching on equalities of pointer-typed variables must have
us consider both of their value sets to be equal. Else we may end up
with spurious counterexamples as seen with the enclosed regression test
(where we previously did not have any known value for `a`).

Fixes: diffblue#8492