Expanded test

viperproject · Oct 22, 2024 · aac52da · aac52da
1 parent 999ef97
commit aac52da
Show file tree

Hide file tree

Showing 2 changed files with 52 additions and 1 deletion.
diff --git 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
@@ -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)