viperproject/gobra#776 introduces the refute statements, simplifies the interface between Gobra and Viper, and fixes a few long-lasting bugs. It is a step in the right direction.
Nonetheless, I'm undoing this PR for two reasons:
it breaks the chopper, which is an essential feature to work on large codebases. The chopper expects to get the Viper program after all plugins have executed, but this is not the case if we use the SiliconFrontendAPI. Because of this, and because the chopper does not properly handle termination measures, we usually get errors on the chopped parts because the output does not contain the declaration of domains that define termination measures.
There are currently a few bugs with pretty printing the Viper program when --printVpr is passed. In particular, termination measures are printed as requires decreases ... or ensures decreases .... In some cases, I also noticed that the pretty printer insers an @ before a predicate name when a predicate instance is used as a termination measure.
While the errors in the pretty printer could be easily solved with a few hacks (in silver), the issue with the chopper is a major dealbreaker. I think the proper solution to this requires promoting termination checking from a Viper plugin to a first-class feature in Viper. Maintaining termination support as a plugin will only lead to hacky solutions.
After the Viper issues are addressed, I would be happy to remerge this PR in its entirety
viperproject/gobra#776 introduces the
refutestatements, simplifies the interface between Gobra and Viper, and fixes a few long-lasting bugs. It is a step in the right direction.Nonetheless, I'm undoing this PR for two reasons:
SiliconFrontendAPI. Because of this, and because the chopper does not properly handle termination measures, we usually get errors on the chopped parts because the output does not contain the declaration of domains that define termination measures.--printVpris passed. In particular, termination measures are printed asrequires decreases ...orensures decreases .... In some cases, I also noticed that the pretty printer insers an@before a predicate name when a predicate instance is used as a termination measure.While the errors in the pretty printer could be easily solved with a few hacks (in silver), the issue with the chopper is a major dealbreaker. I think the proper solution to this requires promoting termination checking from a Viper plugin to a first-class feature in Viper. Maintaining termination support as a plugin will only lead to hacky solutions.
After the Viper issues are addressed, I would be happy to remerge this PR in its entirety