diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala index 367edc4b9..3eb934129 100644 --- a/src/main/scala/viper/silver/ast/Program.scala +++ b/src/main/scala/viper/silver/ast/Program.scala @@ -427,7 +427,7 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se (if (!((formalArgs ++ formalReturns) forall (_.typ.isConcrete))) Seq(ConsistencyError("Formal args and returns must have concrete types.", pos)) else Seq()) ++ (pres ++ posts).flatMap(Consistency.checkNoPermForpermExceptInhaleExhale) ++ checkReturnsNotUsedInPreconditions ++ - (pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, false)) ++ + (pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, false)) lazy val checkReturnsNotUsedInPreconditions: Seq[ConsistencyError] = { val varsInPreconditions: Seq[LocalVar] = pres flatMap {_.deepCollect {case l: LocalVar => l}} diff --git a/src/test/resources/all/functions/function_precondition_perms.vpr b/src/test/resources/all/functions/function_precondition_perms.vpr index 84a8feac2..d9e5dc8c1 100644 --- a/src/test/resources/all/functions/function_precondition_perms.vpr +++ b/src/test/resources/all/functions/function_precondition_perms.vpr @@ -18,6 +18,9 @@ function foop(x: Ref): Int function foo2(x: Ref, b: Bool): Int requires acc(x.f, b ? write : none) +function foo2w(x: Ref, b: Bool): Int + requires acc(x.f, b ? wildcard : none) + function foo3(x: Ref): Int requires acc(x.f, wildcard) @@ -226,6 +229,54 @@ method test3qp(x: Ref, b: Bool) tmp := foo2(x, !b) } +method test2w(x: Ref, b: Bool) +{ + inhale acc(x.f, b ? 1/2 : none) + var tmp: Int + tmp := foo2w(x, b) +} + +@exhaleMode("mce") +method test2mcew(x: Ref, b: Bool) +{ + inhale acc(x.f, b ? 1/2 : none) + var tmp: Int + tmp := foo2w(x, b) +} + +method test2qpw(x: Ref, b: Bool) +{ + inhale forall y: Ref :: y == x ==> acc(y.f, b ? 1/2 : none) + var tmp: Int + tmp := foo2w(x, b) +} + + +method test3w(x: Ref, b: Bool) +{ + inhale acc(x.f, b ? 1/2 : none) + var tmp: Int + //:: ExpectedOutput(application.precondition:insufficient.permission) + tmp := foo2w(x, !b) +} + +@exhaleMode("mce") +method test3mcew(x: Ref, b: Bool) +{ + inhale acc(x.f, b ? 1/2 : none) + var tmp: Int + //:: ExpectedOutput(application.precondition:insufficient.permission) + tmp := foo2w(x, !b) +} + +method test3qpw(x: Ref, b: Bool) +{ + inhale forall y: Ref :: y == x ==> acc(y.f, b ? 1/2 : none) + var tmp: Int + //:: ExpectedOutput(application.precondition:insufficient.permission) + tmp := foo2w(x, !b) +} + method test4(x: Ref) { inhale acc(x.f, 1/2)