goblint / analyzer

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

Union: `meet` in `Field`: Do not raise `Uncomparable` when one arg is `Top` #1471

Closed michael-schwarz closed 4 months ago

michael-schwarz commented 4 months ago

This behavior leads to unnecessary imprecision in combination with the invariant refinement for privatizations at branches.

This was added in https://github.com/goblint/analyzer/pull/1109 but it seems we were a bit overzealous in raising this exception even if one of the arguments is Top.

This fixes some of the issues described in #1456.