goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Fix `BaseDomain` top `priv` typo #1463

Closed sim642 closed 1 month ago

sim642 commented 1 month ago

While having a quick look at the alternative fix in https://github.com/goblint/analyzer/pull/1458#discussion_r1599661735, I spotted that BaseDomain's top has a typo: it has been copied from bot but the priv field hasn't been updated.

is_top also suggests that it should be this way: https://github.com/goblint/analyzer/blob/6783a4db6477d5cc9bd5d65bbe08c175c9c4f5fa/src/cdomains/baseDomain.ml#L96

Inserting assert false there and running all our tests reveals that it never even gets used, so this doesn't have any surprising consequences. Still, it's better to have things consistent, even if they're currently unused and only there to satisfy the signature.

sim642 commented 1 month ago

I had deja vu about this. Turns out this came up once before: https://github.com/goblint/analyzer/pull/1095/files#r1246640502.