dafny-mode fails to parse warnings

[SohumB]

This is my file:

function fib(n: int): int {
  if n in {0,1}
    then 1
    else fib(n-1) + fib(n-2)
}

Running dafny on it produces the following error:

$ dafny /compile\:0 /nologo /home/sohum/tmp/1fib.dfy
/home/sohum/tmp/1fib.dfy(4,9): Error: decreases expression must be bounded below by 0
/home/sohum/tmp/1fib.dfy(1,13): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon7_Else
    (0,0): anon8_Else

Dafny program verifier finished with 0 verified, 1 error

Compilation exited abnormally with code 3 at Tue Sep 27 14:45:48

dafny-mode however crashes on it and reports no errors, showing this stack trace:

Debugger entered--Lisp error: (wrong-type-argument arrayp nil)
  replace-regexp-in-string("/home/sohum/tmp/flycheck_1fib\\.dfy" "/home/sohum/tmp/1fib.dfy" nil fixed-case literal)
  flycheck-fix-error-filename([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil] ("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/")
  #[257 "\302
\300\301#\207" [("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/" flycheck-fix-error-filename] 5 "\n\n(fn E)"]([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil])
  seq-map(#[257 "\302
\300\301#\207" [("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/" flycheck-fix-error-filename] 5 "\n\n(fn E)"] ([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 9 "decreases n" tooltip nil] [cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 4 9 "decreases expression must be bounded below by 0" error nil] [cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil]))
  flycheck-finish-checker-process(dafny 3 ("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/flycheck_1fib.dfy(1,9): Info: decreases n\n/home/sohum/tmp/flycheck_1fib.dfy(4,9): Error: decreases expression must be bounded below by 0\n/home/sohum/tmp/flycheck_1fib.dfy(1,13): Related location\nExecution trace:\n    (0,0): anon0\n    (0,0): anon7_Else\n    (0,0): anon8_Else\n\nDafny program verifier finished with 0 verified, 1 error\n" #[128 "\301\302\300#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/")
  #[0 "\304\300!\211\305=\203\302\306!\202)\211\307=\203(\310\311\300\312\"\313\300!\301\314\300!\302\303&\202)\315\207" [#<process flycheck-dafny> ("/home/sohum/tmp/flycheck_1fib.dfy") #[128 "\301\302\300#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/" process-status signal interrupted exit flycheck-finish-checker-process process-get flycheck-checker process-exit-status flycheck-get-output nil] 8 "\n\n(fn)"]()
  funcall(#[0 "\304\300!\211\305=\203\302\306!\202)\211\307=\203(\310\311\300\312\"\313\300!\301\314\300!\302\303&\202)\315\207" [#<process flycheck-dafny> ("/home/sohum/tmp/flycheck_1fib.dfy") #[128 "\301\302\300#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/" process-status signal interrupted exit flycheck-finish-checker-process process-get flycheck-checker process-exit-status flycheck-get-output nil] 8 "\n\n(fn)"])
  flycheck-handle-signal(#<process flycheck-dafny> "exited abnormally with code 3\n")

It looks like the structure returned as the warning doesn't include the (flycheck-error-message).

[cpitclaudel]

Thanks for the report; I need quite a bit more info to be able to debug this though :)

• Which version of Emacs and Dafny are you using?
• Are you using the inferior Dafny mode (with the Dafny server) or just the plain Dafny tool?

Clément.

[SohumB]

Emacs 25.4, dafny 1.9.7, and the plain cli tool.

On Tue, 27 Sep 2016, 16:51 Clément Pit--Claudel, notifications@github.com wrote:

Thanks for the report; I need quite a bit more info to be able to debug this though :)

• Which version of Emacs and Dafny are you using?
• Are you using the inferior Dafny mode (with the Dafny server) or just the plain Dafny tool?

Clément.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/boogie-org/boogie-friends/issues/11#issuecomment-250032364, or mute the thread https://github.com/notifications/unsubscribe-auth/AAEDqO08lSHOb9ht1Xt3giosP7ja6FZGks5quavngaJpZM4KINfo .

[cpitclaudel]

25.4

Uh?

[cpitclaudel]

Also: thanks! Reproduced :) This is really silly. I mostly use the server checker, so I missed that. Working on a fix now.

[cpitclaudel]

Ok. It's an upstream Flycheck issue introduced in flycheck/flycheck@a8147c47be11d2e904dc2be6c522aec717aa4d57

[cpitclaudel]

https://github.com/flycheck/flycheck/pull/1114

[SohumB]

My apologies, 24.5 :p Thanks for the quick debugging!

[cpitclaudel]

24.5

:)

Btw, things should work fine if you use the more efficient inferior-dafny-mode (use M-x customize-group RET dafny RET and pick server in the last option). With this on, Dafny will run as a local server process on your machine, and cache verification results as you write your program.