analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Sanity check both branches not dead

Open sim642 opened this issue 1 year ago • 0 comments

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.

sim642 avatar Aug 22 '22 09:08 sim642