Block.jump_= deparents the existing Jump and updates the parent for the replacement Jump. This breaks things if a Jump that is already contained within another Block is the input Jump, as the reference to it in its previous Block will not be removed. Then, if the previous Block's Jump is updated, its old Jump (which already has a different parent) will have its parent set to None which further breaks things.
Either Jump.deParent() should replace a Block's jump with some dummy Jump (maybe just None?) or Block.jump_= should prevent a Jump contained within an existing Block being used as input, though that would probably require a way to safely decouple a Jump from its parent Block too?
replaceJump is also redundant given that jump_= exists?
l-kent
commented
3 months ago
https://github.com/UQ-PAC/bil-to-boogie-translator/blob/b6a2409f60b977985ee0c97959cdcfe04bdb35f0/src/main/scala/ir/Program.scala#L380-L386
Block.jump_=deparents the existing Jump and updates the parent for the replacement Jump. This breaks things if a Jump that is already contained within another Block is the input Jump, as the reference to it in its previous Block will not be removed. Then, if the previous Block's Jump is updated, its old Jump (which already has a different parent) will have its parent set to None which further breaks things.Either
Jump.deParent()should replace a Block's jump with some dummy Jump (maybe just None?) orBlock.jump_=should prevent a Jump contained within an existing Block being used as input, though that would probably require a way to safely decouple a Jump from its parent Block too?replaceJumpis also redundant given thatjump_=exists?