summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorD. Ben Knoble <ben.knoble+github@gmail.com>2020-11-30 13:40:57 -0500
committerD. Ben Knoble <ben.knoble+github@gmail.com>2020-11-30 13:40:57 -0500
commit303b89a6b4ace2ee41818499b958a2f486e8864c (patch)
treef9acd38ce3391998b7965d993122b6a1d46fcd89 /test
parent3f01cc247c200850046f59676b0dfead22986f9b (diff)
downloadale-303b89a6b4ace2ee41818499b958a2f486e8864c.zip
add tests
Diffstat (limited to 'test')
-rw-r--r--test/handler/test_dafny_handler.vader12
1 files changed, 10 insertions, 2 deletions
diff --git a/test/handler/test_dafny_handler.vader b/test/handler/test_dafny_handler.vader
index 674f691d..75567414 100644
--- a/test/handler/test_dafny_handler.vader
+++ b/test/handler/test_dafny_handler.vader
@@ -20,9 +20,17 @@ Execute(The Dafny handler should parse output correctly):
\ 'lnum': 678,
\ 'text': 'This is the precondition that might not hold.',
\ '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, [
\ '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",
\ ])