2017-11-15 17:21:17 +00:00
|
|
|
Before:
|
2017-11-08 06:11:49 +00:00
|
|
|
runtime ale_linters/dafny/dafny.vim
|
2017-11-15 17:21:17 +00:00
|
|
|
|
|
|
|
After:
|
|
|
|
call ale#linter#Reset()
|
|
|
|
|
|
|
|
Execute(The Dafny handler should parse output correctly):
|
2017-11-08 06:11:49 +00:00
|
|
|
AssertEqual
|
|
|
|
\ [
|
|
|
|
\ {
|
2020-10-08 16:02:30 +00:00
|
|
|
\ 'filename': 'File.dfy',
|
2017-11-08 06:11:49 +00:00
|
|
|
\ 'col': 45,
|
|
|
|
\ 'lnum': 123,
|
|
|
|
\ 'text': 'A precondition for this call might not hold.',
|
|
|
|
\ 'type': 'E'
|
|
|
|
\ },
|
|
|
|
\ {
|
2020-10-08 16:02:30 +00:00
|
|
|
\ 'filename': 'File.dfy',
|
2017-11-08 06:11:49 +00:00
|
|
|
\ 'col': 90,
|
|
|
|
\ 'lnum': 678,
|
|
|
|
\ 'text': 'This is the precondition that might not hold.',
|
|
|
|
\ 'type': 'W'
|
2020-11-30 18:40:57 +00:00
|
|
|
\ },
|
|
|
|
\ {
|
2021-01-23 17:34:36 +00:00
|
|
|
\ 'filename': 'File.dfy',
|
2020-11-30 18:40:57 +00:00
|
|
|
\ 'col': 45,
|
|
|
|
\ 'lnum': 123,
|
|
|
|
\ 'text': "Verification of 'Impl$$_22_Proof.__default.PutKeepsMapsFull' timed out after 2 seconds",
|
|
|
|
\ 'type': 'E'
|
|
|
|
\ },
|
2017-11-08 06:11:49 +00:00
|
|
|
\ ],
|
|
|
|
\ ale_linters#dafny#dafny#Handle(0, [
|
|
|
|
\ 'File.dfy(123,45): Error BP5002: A precondition for this call might not hold.',
|
2020-11-30 18:40:57 +00:00
|
|
|
\ 'File.dfy(678,90): Related location: This is the precondition that might not hold.',
|
|
|
|
\ "File.dfy(123,45): Verification of 'Impl$$_22_Proof.__default.PutKeepsMapsFull' timed out after 2 seconds",
|
2017-11-08 06:11:49 +00:00
|
|
|
\ ])
|