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 | |
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')
-rw-r--r-- | Test/dafny0/one-message-per-failed-precondition.dfy | 20 |
1 files changed, 20 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) }
|