Test for Silicon issue #894 (#839)

src/test/resources/oldpermsemantics/issues/silicon_894.vpr

@@ -0,0 +1,85 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+
+@exhaleMode("mce")
+method foo(x: Ref, y: Ref)
+{
+  inhale acc(x.f) && acc(y.f)
+
+  var myseq: Seq[Ref] := Seq(x, y)
+
+  assert forall r: Ref :: r in myseq ==> fn(r) > 2
+
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
+
+@exhaleMode("mce")
+function fn(x: Ref): Int
+  requires acc(x.f, wildcard)
+{5}
+
+@exhaleMode("mce")
+function foo1(x: Ref, y: Ref, z: Ref, b: Bool): Int
+  requires b ? acc(x.f) : acc(y.f)
+  requires b ? z == x : z == y
+  requires bar(z) > 2
+{5}
+
+@exhaleMode("mce")
+function foo2(x: Ref, y: Ref, z: Ref, b: Bool): Int
+  requires acc(x.f) && acc(y.f)
+  requires z == x || z == y
+  requires bar(z) > 2
+{5}
+
+@exhaleMode("mce")
+function foo3(x: Ref, y: Ref, z: Ref, b: Bool): Int
+  requires acc(x.f, b ? write : none) && acc(y.f, b ? none : write)
+  requires (z == x && b && z != y) || (z == y && !b && z != x)
+  requires bar(z) > 2
+{5}
+
+
+@exhaleMode("mce")
+function bar(x: Ref): Int
+  requires acc(x.f, wildcard)
+{
+  5
+}
+
+@exhaleMode("mce")
+method caller1(x: Ref, y: Ref)
+{
+  inhale acc(x.f) && acc(y.f)
+  var res: Int
+  res := foo1(x, y, x, true)
+  res := foo1(x, y, y, false)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
+
+@exhaleMode("mce")
+method caller2(x: Ref, y: Ref)
+{
+  inhale acc(x.f) && acc(y.f)
+  var res: Int
+  res := foo2(x, y, x, true)
+  res := foo2(x, y, y, false)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
+
+@exhaleMode("mce")
+method caller3(x: Ref, y: Ref)
+{
+  inhale acc(x.f) && acc(y.f)
+  var res: Int
+  res := foo3(x, y, x, true)
+  res := foo3(x, y, y, false)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}