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 | |
| parent | 19c70cd0d7a65c46bcaafa66b13bde43316bc081 (diff) | |
Add a test to check that there are as many errors as failed preconditions
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/one-message-per-failed-precondition.dfy | 20 | ||||
| -rw-r--r-- | Test/dafny0/one-message-per-failed-precondition.dfy.expect | 20 |
2 files changed, 40 insertions, 0 deletions
diff --git a/Test/dafny0/one-message-per-failed-precondition.dfy b/Test/dafny0/one-message-per-failed-precondition.dfy new file mode 100644 index 00000000..ef4f5bd6 --- /dev/null +++ b/Test/dafny0/one-message-per-failed-precondition.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// When a function call violates two preconditions at the same time, it causes
+// two errors to be reported for the same token
+
+method A(x: int)
+ requires x > 0
+ requires x < 0
+{}
+
+method B(x: int) {
+ A(x);
+}
+
+function fA(x: int): int
+ requires x > 0
+ requires x < 0 { 1 }
+
+function fB(x: int): int { fA(x) }
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
|