RepoMirrors
/
ale
mirror of https://github.com/dense-analysis/ale
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

add tests

This commit is contained in:
D. Ben Knoble 2020-11-30 13:40:57 -05:00
parent 3f01cc247c
commit 303b89a6b4
1 changed files with 10 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
test/handler/test_dafny_handler.vader
View File

@ -20,9 +20,17 @@ Execute(The Dafny handler should parse output correctly):
\ 'lnum': 678, \ 'lnum': 678,
\ 'text': 'This is the precondition that might not hold.', \ 'text': 'This is the precondition that might not hold.',
\ 'type': 'W' \ 'type': 'W'
\ } \ },
\ {
\ 'bufnr': 0,
\ 'col': 45,
\ 'lnum': 123,
\ 'text': "Verification of 'Impl$$_22_Proof.__default.PutKeepsMapsFull' timed out after 2 seconds",
\ 'type': 'E'
\ },
\ ], \ ],
\ ale_linters#dafny#dafny#Handle(0, [ \ ale_linters#dafny#dafny#Handle(0, [
\ 'File.dfy(123,45): Error BP5002: A precondition for this call might not hold.', \ 'File.dfy(123,45): Error BP5002: A precondition for this call might not hold.',
\ 'File.dfy(678,90): Related location: This is the precondition that might not hold.' \ '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",
\ ]) \ ])