From 8afb07fb60f9521212066fbbff233c034ee8af40 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 22:17:18 -0700 Subject: Add a test to check that there are as many errors as failed preconditions --- .../one-message-per-failed-precondition.dfy.expect | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 Test/dafny0/one-message-per-failed-precondition.dfy.expect (limited to 'Test/dafny0/one-message-per-failed-precondition.dfy.expect') diff --git a/Test/dafny0/one-message-per-failed-precondition.dfy.expect b/Test/dafny0/one-message-per-failed-precondition.dfy.expect new file mode 100644 index 00000000..0a76965e --- /dev/null +++ b/Test/dafny0/one-message-per-failed-precondition.dfy.expect @@ -0,0 +1,20 @@ +one-message-per-failed-precondition.dfy(13,3): Error BP5002: A precondition for this call might not hold. +one-message-per-failed-precondition.dfy(9,13): Related location: This is the precondition that might not hold. +Execution trace: + (0,0): anon0 +one-message-per-failed-precondition.dfy(13,3): Error BP5002: A precondition for this call might not hold. +one-message-per-failed-precondition.dfy(8,13): Related location: This is the precondition that might not hold. +Execution trace: + (0,0): anon0 +one-message-per-failed-precondition.dfy(20,27): Error: possible violation of function precondition +one-message-per-failed-precondition.dfy(18,13): Related location +Execution trace: + (0,0): anon0 + (0,0): anon4_Else +one-message-per-failed-precondition.dfy(20,27): Error: possible violation of function precondition +one-message-per-failed-precondition.dfy(17,13): Related location +Execution trace: + (0,0): anon0 + (0,0): anon4_Else + +Dafny program verifier finished with 4 verified, 4 errors -- cgit v1.2.3