Imprecise error message when doing inbounds pointer arithmetic on pointer to freed allocation

[DoubleHyphen]

This is probably rather niche, but it seems like a low-hanging fruit.
Here is a code example:

    let x: *const u8 = {
        let a = 0u8;
        &a
    };
    unsafe 
    {
        let x = x.add(0);
    }

Error message

error: Undefined Behavior: pointer to alloc1494 was dereferenced after this allocation got freed

Except… nothing was dereferenced. The pointer's value didn't even change.

From what I gathered by reading the documentation, .add creates immediate UB if it outputs a pointer whose dereferencing would be illegal, which is exactly the case here; indeed, although the value doesn't change, it's UB according to the documentation. But it's not exactly correct to claim that it was dereferenced when it wasn't.

[RalfJung]

Yeah, the code that checks dereferencability and offset-inbounds is shared but clearly we should differentiate this for the error message. We do this successfully (I think) for the message saying that the pointer is no in-bounds, but use-after-free is checked earlier. Probably PointerUseAfterFree should also take a CheckInAllocMsg.

[DoubleHyphen]

Just tried this again on the playground. This time it failed with

error: Undefined Behavior: out-of-bounds pointer arithmetic: alloc1290 has been freed, so this pointer is dangling

which is pretty much all it needs to say. Closing issue as a result.