Extend `kani::mem::same_allocation` for Unit Type Pointers

[xsxszab]

Description
The same_allocation API currently cannot accept pointers to unit types as inputs, doing so will result in verification failures. Extending same_allocation to support unit type pointers would enhance its usability, especially for implementing function contracts involving generic typed pointers. This capability would be particularly valuable for use cases like the one discussed here.

Example

#[kani::proof]
fn test_unit_type() {
    let unit_obj = ();
    let ptr1: *const () = &unit_obj;
    let ptr2: *const () = &unit_obj;
    assert!(kani::mem::same_allocation(ptr1, ptr2));
}

Running Kani on this proof produces the following error:

Failed Checks: Kani does not support reasoning about pointers to unallocated memory.

[celinval]

I believe the problem here is that unit_obj is not allocated because it is a ZST. The code bellow should work though:

#[kani::proof]
fn test_unit_type() {
    let tup_obj = (0u8, ());
    let ptr1: *const () = &tup_obj.1;
    let ptr2: *const () = &tup_obj.1;
    assert!(kani::mem::same_allocation(ptr1, ptr2));
}

[xsxszab]

Got it, we will add extra checks to handle this special case in our function contracts.