diff options
| author |  Rustan Leino <unknown> | 2015-08-20 18:15:24 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-08-20 18:15:24 -0700 |
| commit | c90ce03a868baeb34de89a4fb73c5001dc737bec (patch) | |
| tree | b7e947a8c6d40bce0fce34521cfc1804e6c59fdc /Test/dafny0 | |
| parent | efcd1e908cb7ea05e78faffd206fa5ce1e966b74 (diff) | |
| parent | 24812516d64ed809d7446680a79eac492ea6a201 (diff) | |
Merge
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
|