I checked a few programs in this category, I do not see major blockers, but for a few programs there is one major pain point: they contain irreducible control flow (i.e. goto jumps into the middle of loops), which the BMC algorithm and our recursive CFAs cannot handle. There are some transformations that sometimes can transform irreducible control flow to reducible, but they are very costly and completely unnecessary for normal programs (see #4 ).
I checked a few programs in this category, I do not see major blockers, but for a few programs there is one major pain point: they contain irreducible control flow (i.e. goto jumps into the middle of loops), which the BMC algorithm and our recursive CFAs cannot handle. There are some transformations that sometimes can transform irreducible control flow to reducible, but they are very costly and completely unnecessary for normal programs (see #4 ).