On 64bit architectures those casts would be to unsigned long. When such combined programs are now analyzed by Goblint on a 64bit machine (which all of us do), then Goblint's special handling of ignoring those casts for pointer equality don't apply because the downcast is not injective.
This causes precision problems since branch refinement cannot refine he from {?, NULL} in either branch. This leads to unnecessary NULL/unknown pointer dereferences even if the uncombined program explicitly protects against it.
Here's a NULL pointer check which has been combined by CIL on a 32bit architecture, as indicated by the casts to
unsigned int: https://github.com/goblint/bench/blob/f2dedc3ad942b1c81ef3d5695d781e927ec9e8f9/pthread/aget_comb.c#L934-L941 (Those casts being inserted at all for pointer equality is a whole other mystery to me.)On 64bit architectures those casts would be to
unsigned long. When such combined programs are now analyzed by Goblint on a 64bit machine (which all of us do), then Goblint's special handling of ignoring those casts for pointer equality don't apply because the downcast is not injective.This causes precision problems since branch refinement cannot refine
hefrom{?, NULL}in either branch. This leads to unnecessary NULL/unknown pointer dereferences even if the uncombined program explicitly protects against it.