Make assume impure (#779)

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala

@@ -19,7 +19,7 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl =>
     case PAssert(exp) => assignableToSpec(exp)
     case PRefute(exp) => assignableToSpec(exp)
     case PExhale(exp) => assignableToSpec(exp)
-    case PAssume(exp) => assignableToSpec(exp) ++ isPureExpr(exp)
+    case PAssume(exp) => assignableToSpec(exp)
     case PInhale(exp) => assignableToSpec(exp)
     case PFold(acc) => wellDefFoldable(acc)
     case PUnfold(acc) => wellDefFoldable(acc)

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

@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package assumption
+
+type person struct {
+	name string
+	age  int
+}
+
+func f() {
+	p := &person{name: "Pereira", age: 12}
+	assume acc(p) // impure assume does not lead to contradiction
+	//:: ExpectedOutput(assert_error:assertion_error)
+	assert false
+}
+
+func g() {
+	p := &person{name: "Pereira", age: 12}
+	inhale acc(p) // inhale leads to contradiction
+	assert false
+}