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
- Instead of comparing the identity of the `PointerValue`s, compare the
underlying `StorageLocation`s.
- If the `StorageLocation`s are the same, return a definite "true" as the
result of the comparison. Before, if the `PointerValue`s were different, we
would return an atom, even if the storage locations themselves were the same.
- If the `StorageLocation`s are different, return an atom (as before). Pointers
that have different storage locations may still alias, so we can't return a
definite "false" in this case.
The application-level gains from this are relatively modest. For the Crubit
nullability check running on an internal codebase, this change reduces the
number of functions on which the SAT solver times out from 223 to 221; the
number of "pointer expression not modeled" errors reduces from 3815 to 3778.
Still, it seems that the gain in precision is generally worthwhile.
@Xazax-hun inspired me to think about this with his
[comments](#73860 (review))
on a different PR.
0 commit comments