Warnings not displayed

[ArquintL]

As observed by @marcoeilers, Viper-IDE currently does not seem to display any warnings (neither parser nor type-checker warnings).

This is an example that contains 1 parser and 1 type-checker warnings:

define macro(x) { assert true }

method test() {
    macro(5)
}

domain PMap[K,T] {
  function dom(p:PMap[K,T]) : Set[K]
  function empty() : PMap[K,T]
  axiom empty_dom { forall k:K :: { k in dom(empty()) } k in dom(empty()) ==> false }
}

[marcoeilers]

I looked into this a little bit (if this is an easy fix, I'd really like to fix this for the release), but I don't really know the ViperServer/IDE code bases at all.

Which of the two "frontends" of ViperServer is currently used by the IDE, the frontends/http or the frontends/lsp one? Did we maybe switch from one to the other? Unlike the HTTP frontend (https://github.com/viperproject/viperserver/blob/7592927254b787b597a6688341a5aaa942f95445/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala#L433C61-L433C82), the LSP frontend (https://github.com/viperproject/viperserver/blob/7592927254b787b597a6688341a5aaa942f95445/src/main/scala/viper/server/frontends/lsp/FileManager.scala#L247C20-L247C20) does not seem to have any cases for the three types of warning messages (WarningsDuringParsing, WarningsDuringTypechecking, WarningsDuringVerification is new) we currently have. So if we're using that, I'm pretty sure that's why warnings aren't working.

[ArquintL]

Yes, Viper-IDE switched to LSP a while ago. What one would have to do is to turn these warning messages into diagnostic items with severity ‚warning‘

[marcoeilers]

Great, thanks, then I think/hope I can take care of this.