Add tests for refute

src/test/resources/regressions/features/refute/refute-fail-01.gobra

@@ -0,0 +1,24 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package refutation
+
+func f() {
+    //:: ExpectedOutput(type_error)
+	refute 3
+}
+
+func g() {
+    x@ := 0
+	//:: ExpectedOutput(type_error)
+	refute &x
+}
+
+func nonPureFunc() bool {
+    return true
+}
+
+func h() {
+    //:: ExpectedOutput(type_error)
+    refute nonPureFunc()
+}

src/test/resources/regressions/features/refute/refute-fail-02.gobra

@@ -0,0 +1,40 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package refutation
+
+func f() {
+    //:: ExpectedOutput(refute_error:refutation_true_error)
+	refute true
+}
+
+func g() {
+    assume false
+    //:: ExpectedOutput(refute_error:refutation_true_error)
+    refute false
+}
+
+requires x > 0
+func h(x int) {
+    //:: ExpectedOutput(refute_error:refutation_true_error)
+	refute x > 0
+}
+
+requires acc(x)
+func i(x *int) {
+    //:: ExpectedOutput(refute_error:refutation_true_error)
+    refute acc(x)
+}
+
+ensures res == x + 1
+pure
+func inc(x int) (res int) {
+    return x + 1
+}
+
+func clientInc() {
+    x := 0
+    y := inc(x)
+    //:: ExpectedOutput(refute_error:refutation_true_error)
+    refute y == 1
+}

src/test/resources/regressions/features/refute/refute-simple-01.gobra

@@ -0,0 +1,50 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package refutation
+
+func f() {
+    refute false
+}
+
+requires x > 0
+func g(x int) {
+    refute x < 0
+}
+
+func h(x *int) {
+    refute acc(x)
+}
+
+func i(cond bool) {
+    x := 0
+
+    if (cond) {
+        x := 1
+    }
+
+    refute x == 1
+}
+
+decreases
+pure
+func falseFunc() bool {
+    return false
+}
+
+func clientFalseFunc() {
+    refute falseFunc()
+}
+
+ensures res == x + 1
+decreases
+pure
+func inc(x int) (res int) {
+    return x + 1
+}
+
+func clientInc() {
+    x := 0
+    y := inc(x)
+    refute y != 1
+}