Adding tests

src/test/resources/all/asserting/function.vpr

@@ -0,0 +1,38 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function fplusone(x: Ref, y: Ref): Int
+    requires acc(x.f)
+{
+  asserting (x != null) in (x.f + 1)
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fplusone2(x: Ref, y: Ref): Int
+    requires acc(x.f)
+{
+  asserting (x != y) in (x.f + 1)
+}
+
+method main()
+{
+  var x: Ref
+  x := new(f)
+
+  var hmm: Int
+  hmm := fplusone(x, x)
+  hmm := asserting (hmm == x.f + 1) in hmm
+}
+
+method main2()
+{
+  var x: Ref
+  x := new(f)
+
+  var hmm: Int
+  hmm := fplusone(x, x)
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  hmm := asserting (hmm == x.f) in hmm
+}

src/test/resources/all/asserting/other-fail.vpr

@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field x: Int
+
+method test1() {
+  //:: ExpectedOutput(assert.failed:division.by.zero)
+  assert asserting (1 / 0 == 0) in true
+}
+
+method test2() {
+  //:: ExpectedOutput(assert.failed:division.by.zero)
+  assert asserting (true) in (1 / 0 == 0)
+}
+
+method test3(r: Ref) {
+  //:: ExpectedOutput(assert.failed:insufficient.permission)
+  assert asserting (true && acc(r.x)) in true
+}

src/test/resources/all/asserting/qp.vpr

@@ -0,0 +1,44 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method m1(s: Set[Ref])
+  requires |s| > 0
+{
+  inhale forall x: Ref :: x in (asserting(|s| > 0) in s) ==> acc(x.f)
+}
+
+method m1Fail(s: Set[Ref])
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in (asserting(|s| > 0) in s) ==> acc(x.f)
+}
+
+method m2(s: Set[Ref])
+  requires |s| > 0
+  requires !(null in s)
+{
+  inhale forall x: Ref :: x in s ==> acc((asserting (x != null) in x).f)
+}
+
+method m2Fail(s: Set[Ref])
+  requires |s| > 0
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in s ==> acc((asserting (x != null) in x).f)
+}
+
+method m3(s: Set[Ref])
+  requires |s| > 0
+  requires !(null in s)
+{
+  inhale forall x: Ref :: x in s ==> acc(x.f, asserting (x != null) in write)
+}
+
+method m3Fail(s: Set[Ref])
+  requires |s| > 0
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in s ==> acc(x.f, asserting (x != null) in write)
+}

src/test/resources/all/asserting/simple-fail.vpr

@@ -0,0 +1,73 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method assign() {
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (false) in 0
+}
+
+method assign2(i: Int) {
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (i > 0) in 0
+}
+
+method assign3(i: Int)
+  requires i > 5
+{
+  var x: Int := asserting (i > 0) in 0
+}
+
+method pres()
+  //:: ExpectedOutput(not.wellformed:assertion.false)
+  requires asserting (false) in false
+{
+  assert false
+}
+
+method pres2(x: Ref)
+  //:: ExpectedOutput(not.wellformed:insufficient.permission)
+  requires asserting (acc(x.f)) in false
+{
+  assert false
+}
+
+method pres3(x: Ref)
+  requires acc(x.f)
+  requires asserting (acc(x.f)) in false
+{
+  assert false
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun(): Int
+{
+  asserting (false) in 0
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function fun2(x: Ref): Int
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun3(x: Ref): Int
+  requires acc(x.f)
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+function fun4(x: Ref): Int
+  requires acc(x.f) && x.f > 8
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+method stateUnchanged(x: Ref)
+  requires acc(x.f)
+{
+  var y: Int := asserting (acc(x.f)) in x.f
+  assert acc(x.f)
+}

src/test/resources/all/asserting/trigger.vpr

@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function trigger(i: Int): Bool
+{
+  true
+}
+
+method triggerUse(s: Seq[Int])
+  requires |s| > 0
+  requires forall i: Int :: {trigger(i)} 0 <= i < |s| ==> s[i] > 0
+{
+  assert asserting (trigger(0)) in s[0] > 0
+}
+
+method triggerUse2(s: Seq[Int])
+  requires |s| > 0
+  requires forall i: Int :: {trigger(i)} 0 <= i < |s| ==> s[i] > 0
+{
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert s[0] > 0
+}

src/test/resources/all/asserting/wand.vpr

@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+field g: Int
+
+method test0(x: Ref)
+{
+    package acc(x.f) && (asserting (acc(x.f)) in (x.f == 0)) --* acc(x.f) {}
+}
+
+method test1(x: Ref)
+{
+    //:: ExpectedOutput(package.failed:insufficient.permission)
+    package acc(x.f) && (asserting (acc(x.g)) in (x.f == 0)) --* acc(x.f) {}
+}
+