{"action":"opened","issue":{"url":"https://api.github.com/repos/boogie-org/boogie-friends/issues/11","repository_url":"https://api.github.com/repos/boogie-org/boogie-friends","labels_url":"https://api.github.com/repos/boogie-org/boogie-friends/issues/11/labels{/name}","comments_url":"https://api.github.com/repos/boogie-org/boogie-friends/issues/11/comments","events_url":"https://api.github.com/repos/boogie-org/boogie-friends/issues/11/events","html_url":"https://github.com/boogie-org/boogie-friends/issues/11","id":179628108,"number":11,"title":"dafny-mode fails to parse warnings","user":{"login":"SohumB","id":66472,"avatar_url":"https://avatars.githubusercontent.com/u/66472?v=3","gravatar_id":"","url":"https://api.github.com/users/SohumB","html_url":"https://github.com/SohumB","followers_url":"https://api.github.com/users/SohumB/followers","following_url":"https://api.github.com/users/SohumB/following{/other_user}","gists_url":"https://api.github.com/users/SohumB/gists{/gist_id}","starred_url":"https://api.github.com/users/SohumB/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SohumB/subscriptions","organizations_url":"https://api.github.com/users/SohumB/orgs","repos_url":"https://api.github.com/users/SohumB/repos","events_url":"https://api.github.com/users/SohumB/events{/privacy}","received_events_url":"https://api.github.com/users/SohumB/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2016-09-27T22:09:07Z","updated_at":"2016-09-27T22:09:07Z","closed_at":null,"body":"This is my file:\r\n```\r\nfunction fib(n: int): int {\r\n  if n in {0,1}\r\n    then 1\r\n    else fib(n-1) + fib(n-2)\r\n}\r\n```\r\n\r\nRunning `dafny` on it produces the following error:\r\n```\r\n$ dafny /compile\\:0 /nologo /home/sohum/tmp/1fib.dfy\r\n/home/sohum/tmp/1fib.dfy(4,9): Error: decreases expression must be bounded below by 0\r\n/home/sohum/tmp/1fib.dfy(1,13): Related location\r\nExecution trace:\r\n    (0,0): anon0\r\n    (0,0): anon7_Else\r\n    (0,0): anon8_Else\r\n\r\nDafny program verifier finished with 0 verified, 1 error\r\n\r\nCompilation exited abnormally with code 3 at Tue Sep 27 14:45:48\r\n```\r\n\r\ndafny-mode however crashes on it and reports no errors, showing this stack trace:\r\n```\r\nDebugger entered--Lisp error: (wrong-type-argument arrayp nil)\r\n  replace-regexp-in-string(\"/home/sohum/tmp/flycheck_1fib\\\\.dfy\" \"/home/sohum/tmp/1fib.dfy\" nil fixed-case literal)\r\n  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/\")\r\n  #[257 \"\\302\u0001\\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])\r\n  seq-map(#[257 \"\\302\u0001\\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]))\r\n  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\u0003#\\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/\")\r\n  #[0 \"\\304\\300!\\211\\305=\\203\u000F\u0000\\302\\306!\\202)\u0000\\211\\307=\\203(\u0000\\310\\311\\300\\312\\\"\\313\\300!\\301\\314\\300!\\302\\303&\u0006\\202)\u0000\\315\\207\" [#<process flycheck-dafny> (\"/home/sohum/tmp/flycheck_1fib.dfy\") #[128 \"\\301\\302\\300\u0003#\\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)\"]()\r\n  funcall(#[0 \"\\304\\300!\\211\\305=\\203\u000F\u0000\\302\\306!\\202)\u0000\\211\\307=\\203(\u0000\\310\\311\\300\\312\\\"\\313\\300!\\301\\314\\300!\\302\\303&\u0006\\202)\u0000\\315\\207\" [#<process flycheck-dafny> (\"/home/sohum/tmp/flycheck_1fib.dfy\") #[128 \"\\301\\302\\300\u0003#\\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)\"])\r\n  flycheck-handle-signal(#<process flycheck-dafny> \"exited abnormally with code 3\\n\")\r\n```\r\n\r\nIt looks like the structure returned as the warning doesn't include the `(flycheck-error-message)`."}}
{"actor":{"display_login":"SohumB"}}