closing: Adding a test while closing issue #370 as out of scope (#793)

Author: davidcok

Test/git-issues/git-issue-370.dfy

@@ -0,0 +1,45 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype T = T(x: int)
+datatype S = S(u: int, v: int, w: int, x: int, y: int, z: int)
+
+predicate a(t: T)
+predicate b(t: T)
+predicate c(t: T)
+predicate d(t: T)
+predicate e(t: T)
+predicate f(t: T)
+predicate g(t: T)
+
+predicate WellFormed(t: T) {
+  && a(t)
+}
+
+function Func(t: T) : S
+requires WellFormed(t)
+{
+  S(t.x, t.x, t.x, t.x, t.x, t.x)
+}
+
+predicate Good(s: S) {
+  && s.u == 5
+  && s.v == 5
+  && s.w == 5
+  && s.x == 5
+  && s.y == 5
+  && s.z == 5
+}
+
+function {:opaque} GetT() : T {
+  T(5)
+}
+
+lemma foo()
+  ensures var t := GetT();
+    && WellFormed(t)
+    && Good(Func(t))
+{
+  reveal_GetT();
+}
+

Test/git-issues/git-issue-370.dfy.expect

@@ -0,0 +1,27 @@
+git-issue-370.dfy(42,0): Error BP5003: A postcondition might not hold on this return path.
+git-issue-370.dfy(40,7): Related location: This is the postcondition that might not hold.
+git-issue-370.dfy(16,5): Related location
+Execution trace:
+    (0,0): anon0
+git-issue-370.dfy(42,0): Error BP5003: A postcondition might not hold on this return path.
+git-issue-370.dfy(41,7): Related location: This is the postcondition that might not hold.
+git-issue-370.dfy(26,9): Related location
+Execution trace:
+    (0,0): anon0
+git-issue-370.dfy(42,0): Error BP5003: A postcondition might not hold on this return path.
+git-issue-370.dfy(41,7): Related location: This is the postcondition that might not hold.
+git-issue-370.dfy(27,9): Related location
+Execution trace:
+    (0,0): anon0
+git-issue-370.dfy(42,0): Error BP5003: A postcondition might not hold on this return path.
+git-issue-370.dfy(41,7): Related location: This is the postcondition that might not hold.
+git-issue-370.dfy(28,9): Related location
+Execution trace:
+    (0,0): anon0
+git-issue-370.dfy(42,0): Error BP5003: A postcondition might not hold on this return path.
+git-issue-370.dfy(41,7): Related location: This is the postcondition that might not hold.
+git-issue-370.dfy(29,9): Related location
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 5 errors