From d8ca29fef019f3be72b457f8dfad9a7b8bdc7069 Mon Sep 17 00:00:00 2001 From: Lea Salome Brugger Date: Tue, 23 Jul 2024 18:14:04 +0200 Subject: [PATCH] Make assume impure --- .../typing/ghost/GhostStmtTyping.scala | 2 +- .../features/assume/assume-simple-01.gobra | 22 +++++++++++++++++++ 2 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 src/test/resources/regressions/features/assume/assume-simple-01.gobra 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