You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
(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.
The text was updated successfully, but these errors were encountered:
Here's a NULL pointer check which has been combined by CIL on a 32bit architecture, as indicated by the casts to
unsigned int
:bench/pthread/aget_comb.c
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.The text was updated successfully, but these errors were encountered: