When Viper indicates that a CFG is not reducible, the produced error is not useful for debugging. There seems to be no position attached to the error, so in Viper IDE, the error is just a single red-underline character at the very beginning of the file (regardless of the actual error source).
Some ways this error could be improved:
- localise the error to the methods which have irreducible CFGs,
- proceed with verification of other methods even if one has an irreducible CFG, and
- more fine-grained: indicate which jump exactly (or set of jumps?) makes the CFG irreducible.
When Viper indicates that a CFG is not reducible, the produced error is not useful for debugging. There seems to be no position attached to the error, so in Viper IDE, the error is just a single red-underline character at the very beginning of the file (regardless of the actual error source).
Some ways this error could be improved: