Contracts can't specify write-only pointers for --uninitialized-check

[BeamRaceMuppet]

When using --uninitialized-check with code contracts, there's no way to make the contract say it only writes the pointer and does not read it. Minimal example:

void set42(int *p)
__CPROVER_requires(__CPROVER_w_ok(p, sizeof(int)))
__CPROVER_ensures(*p == 42)
__CPROVER_assigns(*p)
;

int main()
{
    int x;
    set42(&x);
    assert(x == 42);
    return 0;
}

Run like this:

$ goto-cc set42.c -o set42.gb && goto-instrument --replace-call-with-contract set42 --uninitialized-check set42.gb set42.i.gb && cbmc set42.i.gb

Output:

[...]
** Results:
set42.c function main
[main.assertion.1] line 11 assertion x == 42: SUCCESS
[main.uninitialized_local.1] line 11 use of uninitialized local variable main::1::x: FAILURE

[...]

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

If there is a way to do this, then please consider this bug report a missing documentation bug instead.

CBMC version: 6.3.1