Open
Description
Here's a NULL pointer check which has been combined by CIL on a 32bit architecture, as indicated by the casts to unsigned int
:
Lines 934 to 941 in f2dedc3
(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 he
from {?, NULL}
in either branch. This leads to unnecessary NULL/unknown pointer dereferences even if the uncombined program explicitly protects against it.