diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala index be6569263..922729f74 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala +++ b/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) diff --git a/src/test/resources/regressions/features/assume/assume-simple-01.gobra b/src/test/resources/regressions/features/assume/assume-simple-01.gobra new file mode 100644 index 000000000..3181e40a4 --- /dev/null +++ b/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 +} \ No newline at end of file