diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 22:17:18 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 22:17:18 -0700 |
| commit | 8afb07fb60f9521212066fbbff233c034ee8af40 (patch) | |
| tree | 3426cd69cdabcb1852b337d6f5449ab8d1452148 /Test/dafny0/one-message-per-failed-precondition.dfy.expect | |
| parent | 19c70cd0d7a65c46bcaafa66b13bde43316bc081 (diff) | |
Add a test to check that there are as many errors as failed preconditions
Diffstat (limited to 'Test/dafny0/one-message-per-failed-precondition.dfy.expect')
| -rw-r--r-- | Test/dafny0/one-message-per-failed-precondition.dfy.expect | 20 |
1 files changed, 20 insertions, 0 deletions
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
|