Thread return value cast causes weird unsigned integer underflow

[Robotechnic]

I stumbled accross a wierd overflow that souldn't happen.
With this code:

int main() {
	int *buff = 0;
	return buff[5];
}

And those parameters:

--ana.arrayoob true --ana.int.interval_set true --ana.base.arrays.domain partitioned --ana.base.arrays.nullbytes true --sem.malloc.fail true --set "ana.activated[+]" memOutOfBounds --set "ana.activated[+]"  useAfterFree

I get the following error message:

[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (... .c:6:9-6:16)

But for me, it shouldn't happen as a possibly random value set by the OS, can't be an overflow value. Let alone for an unsigned integer.

[sim642]

This looks like we might still be missing some speculative execution flag somewhere, but I'm not sure where.
As such, it might also be affecting us in SV-COMP NoOverflows.

[sim642]

The warning comes from the thread return value cast to void* here:

analyzer/src/analyses/base.ml

Lines 2055 to 2060 in ff6f52c

	| `Lifted tid when ThreadReturn.is_current ask ->
	(* Evaluate exp and cast the resulting value to the void-pointer-type.
	Casting to the right type here avoids precision loss on joins. *)
	let rv = VD.cast ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in
	man.sideg (V.thread tid) (G.create_thread rv);
	Priv.thread_return ask (priv_getg man.global) (priv_sideg man.sideg) tid st'

It's done to handle thread return value via pthread_join which does pointers only, but here for main this is never (intended to be) done.

I'm not sure what the right fix would be though: we shouldn't just suppress this with speculation because this can actually happen. And this isn't specific to main either: it could happen with any normal thread return as well.