From 8afb07fb60f9521212066fbbff233c034ee8af40 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Wed, 19 Aug 2015 22:17:18 -0700
Subject: Add a test to check that there are as many errors as failed
 preconditions

---
 Test/dafny0/one-message-per-failed-precondition.dfy  | 20 ++++++++++++++++++++
 .../one-message-per-failed-precondition.dfy.expect   | 20 ++++++++++++++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 Test/dafny0/one-message-per-failed-precondition.dfy
 create mode 100644 Test/dafny0/one-message-per-failed-precondition.dfy.expect

(limited to 'Test/dafny0')

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
-- 
cgit v1.2.3