Open
Description
SymDiff does a lot of dumping and reparsing of Boogie programs, which seems be where the tool spends most of its time. This happens in multiple places, including when SymDiff is creating merged programs for the compared procedures.
As far as.I can tell, the reason SymDiff does this in the first place is that the AST is modified in-place, often leading to an ill-formed one, which dumping & reparsing fixes. This could be fixed by properly updating the AST when it is modified.
I also introduced some code that does the same inefficient dumping & reparsing in #9, so I am creating this issue to track that.
Metadata
Metadata
Assignees
Labels
No labels