From 607ef28aadb281ab61a2be493a637126e967a388 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Thu, 29 May 2014 21:41:00 +0200
Subject: Set up the same test infrastructure as in Boogie.

---
 Test/dafny0/Predicates.dfy.expect | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 Test/dafny0/Predicates.dfy.expect

(limited to 'Test/dafny0/Predicates.dfy.expect')

diff --git a/Test/dafny0/Predicates.dfy.expect b/Test/dafny0/Predicates.dfy.expect
new file mode 100644
index 00000000..dac4eb3c
--- /dev/null
+++ b/Test/dafny0/Predicates.dfy.expect
@@ -0,0 +1,27 @@
+Predicates.dfy[B](21,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[B](20,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy(31,9): Related location
+Execution trace:
+    (0,0): anon0
+Predicates.dfy(88,16): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Predicates.dfy(92,14): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Predicates.dfy[Tricky_Full](126,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[Tricky_Full](125,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy(136,7): Related location
+Predicates.dfy[Tricky_Full](116,9): Related location
+Execution trace:
+    (0,0): anon0
+Predicates.dfy(164,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy(163,15): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+Predicates.dfy[Q1](154,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[Q1](153,15): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 52 verified, 6 errors
-- 
cgit v1.2.3