analyzer
analyzer copied to clipboard
Sanity check both branches not dead
Every now and then we've had unsoundness issues at branches which have both (true and false) outgoing edges raise Deadcode
and yield bottom states. We should have a sanity check for this.
After #525, the dead branch reporting uses a flat boolean lattice:
https://github.com/goblint/analyzer/blob/21e59a1ad72c49bf448066123ead989a746334c4/src/framework/constraints.ml#L1118-L1125
Thus the Bot
case would be when neither outgoing edge is live.
As the comment mentions, only problem is our Neg(1)
edges, which don't have a corresponding Pos(1)
, so the single false branch being trivially dead means that there's also a Bot
.