Closed zgrannan closed 10 months ago
@marcoeilers Probably not very controversial but wanted to double-check with you. This is necessary for the VSCode plugin to work with custom verifiers.
Yes, this looks fine to me, though I know very little about Viper server. It would be better to ask @ArquintL and/or @rayman2000.
@zgrannan doesn't one have to use "custom" as the backend name when one wants to pass a class name that should be used as backend? I'm just wondering whether we can slightly relax the backend name check to also permit "custom" as opposed to completely remove it
@ArquintL Sorry for the late response. Here it's expected to be the classname of the custom verifier. For example for Alex's program verification course at UBC, the value of backendClassName
is core.MyVerifierFrontend
. So I don't think there's any other way to check that a custom verifier should be used, and requiring that the backendClassName
be custom
or contains Custom
might be a bit restrictive?
The className is passed in as backend
here: https://github.com/viperproject/viperserver/blob/6400a3eec5a3e89e57e2dfef109dbf4604617f59/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala#L82, btw.
Sorry, I thought that one has to use "custom <backend name> <args>"
as opposed to, e.g., "silicon <args>"
.
While this seems to be the case when using Viper directly, ViperServer actually provides a nicer wrapper (see object ViperBackendConfig
and trait ViperBackendConfig
in ViperBackendConfig.scala
). That's where the confusion was coming from.
Hence, a custom backend can be selected by using "<backend name> <args>"
when using ViperServer. Therefore, this PR totally makes sense
Using a custom backend in LSP interaction seems to fail because only
silicon
orcarbon
are acceptable as backends ingetVerificationCommand
. This PR lifts this restriction.