viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link

Report verification as successful when there are warnings but not errors #189

Closed marcoeilers closed 10 months ago

marcoeilers commented 10 months ago

This addresses https://github.com/viperproject/viper-ide/issues/412 and matches the behavior of other tools (e.g. compilers): If there are warnings but no errors, we report the warnings, but the overall verification is marked as a success.

As a result, a program that generates no errors but two warnings leads to a result (displayed in VSCode at the bottom left) that is marked as yellow but starts with a checkmark and states "Successfully verified test.vpr in 0.6 seconds with 2 warnings.". Previously, in this situation, VSCode would report a yellow message marked with a cross stating "Verifying test.vpr failed after 0.8 seconds with 0 errors and 2 warnings."

A result of e.g. one error and two warnings still leads to a red result with a cross saying "Verifying test.vpr failed after 0.6 seconds with 1 error and 2 warnings."