From a06efe037aa2da7fa815e7b914a236762e58b577 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 26 Sep 2024 21:01:20 +0200
Subject: [PATCH 01/12] asserting (a) in e

---
 src/main/scala/viper/silver/ast/Expression.scala         | 5 +++++
 .../scala/viper/silver/ast/pretty/PrettyPrinter.scala    | 2 ++
 .../scala/viper/silver/ast/utility/Expressions.scala     | 5 ++++-
 src/main/scala/viper/silver/ast/utility/Nodes.scala      | 1 +
 src/main/scala/viper/silver/parser/FastParser.scala      | 9 +++++++--
 src/main/scala/viper/silver/parser/ParseAst.scala        | 6 ++++++
 src/main/scala/viper/silver/parser/ParseAstKeyword.scala | 2 ++
 src/main/scala/viper/silver/parser/Translator.scala      | 2 ++
 8 files changed, 29 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 0d206d9ae..1b64f482b 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -499,6 +499,11 @@ case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition,
   lazy val typ = body.typ
 }
 
+case class Asserting(a: Exp, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
+  override lazy val check: Seq[ConsistencyError] = Consistency.checkPure(body)
+  lazy val typ = body.typ
+}
+
 // --- Old expressions
 
 sealed trait OldExp extends UnExp {
diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
index 2003fd387..64e1db3f4 100644
--- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -771,6 +771,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
         group(parens(text("unfolding") <+> nest(defaultIndent, show(acc)) <+> "in" <> nest(defaultIndent, line <> show(exp))))
       case Applying(wand, exp) =>
         parens(text("applying") <+> nest(defaultIndent, show(wand)) <+> "in" <> nest(defaultIndent, line <> show(exp)))
+      case Asserting(ass, exp) =>
+        parens(text("asserting") <+> nest(defaultIndent, parens(show(ass))) <+> "in" <> nest(defaultIndent, line <> show(exp)))
       case Old(exp) =>
         text("old") <> parens(show(exp))
       case LabelledOld(exp,label) =>
diff --git a/src/main/scala/viper/silver/ast/utility/Expressions.scala b/src/main/scala/viper/silver/ast/utility/Expressions.scala
index b4fa7c980..df83efbae 100644
--- a/src/main/scala/viper/silver/ast/utility/Expressions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Expressions.scala
@@ -25,6 +25,7 @@ object Expressions {
     case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
     case unf: Unfolding => isPure(unf.body)
     case app: Applying => isPure(app.body)
+    case Asserting(a, e) => isPure(e)
     case QuantifiedExp(_, e0) => isPure(e0)
     case Let(_, _, body) => isPure(body)
     case e: ExtensionExp => e.extensionIsPure
@@ -96,9 +97,10 @@ object Expressions {
   def asBooleanExp(e: Exp): Exp = {
     e.transform({
       case _: AccessPredicate | _: MagicWand => TrueLit()()
-      case fa@Forall(vs,ts,body) => Forall(vs,ts,asBooleanExp(body))(fa.pos,fa.info)
+      case fa@Forall(vs,ts,body) => Forall(vs, ts, asBooleanExp(body))(fa.pos, fa.info, fa.errT)
       case Unfolding(_, exp) => asBooleanExp(exp)
       case Applying(_, exp) => asBooleanExp(exp)
+      case ass@Asserting(a, exp) => Asserting(asBooleanExp(a), asBooleanExp(exp))(ass.pos, ass.info, ass.errT)
     })
   }
 
@@ -199,6 +201,7 @@ object Expressions {
           case MapLookup(m, k) => List(MapContains(k, m)(p))
           case Unfolding(pred, _) => List(pred)
           case Applying(wand, _) => List(wand)
+          case Asserting(a, _) => List(a)
           case _ => Nil
         }
         // Only use non-trivial conditions for the subnodes.
diff --git a/src/main/scala/viper/silver/ast/utility/Nodes.scala b/src/main/scala/viper/silver/ast/utility/Nodes.scala
index 0dc99d7dd..53759e73c 100644
--- a/src/main/scala/viper/silver/ast/utility/Nodes.scala
+++ b/src/main/scala/viper/silver/ast/utility/Nodes.scala
@@ -83,6 +83,7 @@ object Nodes {
           case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc, perm)
           case Unfolding(acc, body) => Seq(acc, body)
           case Applying(wand, body) => Seq(wand, body)
+          case Asserting(ass, body) => Seq(ass, body)
           case Old(exp) => Seq(exp)
           case CondExp(cond, thn, els) => Seq(cond, thn, els)
           case Let(v, exp, body) => Seq(v, exp, body)
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index dfc503ef5..eae845045 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -152,7 +152,7 @@ object FastParserCompanion {
     // maps
     PKw.Map, PKwOp.Range, PKwOp.Domain,
     // prover hint expressions
-    PKwOp.Unfolding, PKwOp.In, PKwOp.Applying,
+    PKwOp.Unfolding, PKwOp.In, PKwOp.Applying, PKwOp.Asserting,
     // old expression
     PKwOp.Old, PKw.Lhs,
     // other expressions
@@ -365,7 +365,7 @@ class FastParser {
   def atomReservedKw[$: P]: P[PExp] = {
     reservedKwMany(
       StringIn("true", "false", "null", "old", "result", "acc", "none", "wildcard", "write", "epsilon", "perm", "let", "forall", "exists", "forperm",
-        "unfolding", "applying", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
+        "unfolding", "applying", "asserting", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
       str => pos => str match {
         case "true" => Pass.map(_ => PBoolLit(PReserved(PKw.True)(pos))(_))
         case "false" => Pass.map(_ => PBoolLit(PReserved(PKw.False)(pos))(_))
@@ -384,6 +384,7 @@ class FastParser {
         case "forperm" => forperm.map(_(PReserved(PKw.Forperm)(pos)))
         case "unfolding" => unfolding.map(_(PReserved(PKwOp.Unfolding)(pos)))
         case "applying" => applying.map(_(PReserved(PKwOp.Applying)(pos)))
+        case "asserting" => asserting.map(_(PReserved(PKwOp.Asserting)(pos)))
         case "Set" => setConstructor.map(_(PReserved(PKwOp.Set)(pos)))
         case "Seq" => seqConstructor.map(_(PReserved(PKwOp.Seq)(pos)))
         case "Multiset" => multisetConstructor.map(_(PReserved(PKwOp.Multiset)(pos)))
@@ -652,6 +653,10 @@ class FastParser {
       PApplying(_, wand.inner, op, b)
   }
 
+  def asserting[$: P]: P[PKwOp.Asserting => Pos => PExp] = P(exp.parens ~ PKwOp.In ~ exp).map {
+    case (a, in, b) => PAsserting(_, a.inner, in, b)
+  }
+
   def predicateAccessAssertion[$: P]: P[PAccAssertion] = P(accessPred | predAcc)
 
   def setConstructor[$: P]: P[PKwOp.Set => Pos => PExp] =
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 4e59f54c4..cc4fd40d5 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1080,6 +1080,12 @@ case class PApplying(applying: PKwOp.Applying, wand: PExp, in: PKwOp.In, exp: PE
     List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
 }
 
+case class PAsserting(asserting: PKwOp.Asserting, a: PExp, in: PKwOp.In, exp: PExp)(val pos: (Position, Position)) extends PHeapOpApp {
+  override val args = Seq(a, exp)
+  override val signatures: List[PTypeSubstitution] =
+    List(Map(POpApp.pArgS(0) -> Impure, POpApp.pResS -> POpApp.pArg(1)))
+}
+
 sealed trait PBinder extends PExp with PScope {
   def boundVars: Seq[PLogicalVarDecl]
 
diff --git a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
index 646c14819..daed9a67f 100644
--- a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
+++ b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
@@ -494,6 +494,8 @@ object PKwOp {
   type Unfolding = PReserved[Unfolding.type]
   case object Applying    extends PKwOp("applying")                 with PKeywordAtom with RightSpace
   type Applying = PReserved[Applying.type]
+  case object Asserting   extends PKwOp("asserting")                with PKeywordAtom with RightSpace
+  type Asserting = PReserved[Asserting.type]
   case object Let         extends PKwOp("let")                      with PKeywordAtom with RightSpace
   type Let = PReserved[Let.type]
 
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 4a6f469d2..91653fb3d 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -513,6 +513,8 @@ case class Translator(program: PProgram) {
         Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos, info)
       case PApplying(_, wand, _, e) =>
         Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos, info)
+      case PAsserting(_, a, _, e) =>
+        Asserting(exp(a), exp(e))(pos, info)
       case pl@PLet(_, _, _, exp1, _, PLetNestedScope(body)) =>
         Let(liftLogicalDecl(pl.decl), exp(exp1.inner), exp(body))(pos, info)
       case _: PLetNestedScope =>

From f649c0baf2fc133a5d99261dbb567b8a33732588 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 27 Sep 2024 10:53:00 +0200
Subject: [PATCH 02/12] Adding tests

---
 src/test/resources/all/asserting/function.vpr | 38 ++++++++++
 .../resources/all/asserting/other-fail.vpr    | 19 +++++
 src/test/resources/all/asserting/qp.vpr       | 44 +++++++++++
 .../resources/all/asserting/simple-fail.vpr   | 73 +++++++++++++++++++
 src/test/resources/all/asserting/trigger.vpr  | 22 ++++++
 src/test/resources/all/asserting/wand.vpr     | 17 +++++
 6 files changed, 213 insertions(+)
 create mode 100644 src/test/resources/all/asserting/function.vpr
 create mode 100644 src/test/resources/all/asserting/other-fail.vpr
 create mode 100644 src/test/resources/all/asserting/qp.vpr
 create mode 100644 src/test/resources/all/asserting/simple-fail.vpr
 create mode 100644 src/test/resources/all/asserting/trigger.vpr
 create mode 100644 src/test/resources/all/asserting/wand.vpr

diff --git a/src/test/resources/all/asserting/function.vpr b/src/test/resources/all/asserting/function.vpr
new file mode 100644
index 000000000..144a7e4ab
--- /dev/null
+++ b/src/test/resources/all/asserting/function.vpr
@@ -0,0 +1,38 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function fplusone(x: Ref, y: Ref): Int
+    requires acc(x.f)
+{
+  asserting (x != null) in (x.f + 1)
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fplusone2(x: Ref, y: Ref): Int
+    requires acc(x.f)
+{
+  asserting (x != y) in (x.f + 1)
+}
+
+method main()
+{
+  var x: Ref
+  x := new(f)
+
+  var hmm: Int
+  hmm := fplusone(x, x)
+  hmm := asserting (hmm == x.f + 1) in hmm
+}
+
+method main2()
+{
+  var x: Ref
+  x := new(f)
+
+  var hmm: Int
+  hmm := fplusone(x, x)
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  hmm := asserting (hmm == x.f) in hmm
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/other-fail.vpr b/src/test/resources/all/asserting/other-fail.vpr
new file mode 100644
index 000000000..465a83c9e
--- /dev/null
+++ b/src/test/resources/all/asserting/other-fail.vpr
@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field x: Int
+
+method test1() {
+  //:: ExpectedOutput(assert.failed:division.by.zero)
+  assert asserting (1 / 0 == 0) in true
+}
+
+method test2() {
+  //:: ExpectedOutput(assert.failed:division.by.zero)
+  assert asserting (true) in (1 / 0 == 0)
+}
+
+method test3(r: Ref) {
+  //:: ExpectedOutput(assert.failed:insufficient.permission)
+  assert asserting (true && acc(r.x)) in true
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/qp.vpr b/src/test/resources/all/asserting/qp.vpr
new file mode 100644
index 000000000..474714a95
--- /dev/null
+++ b/src/test/resources/all/asserting/qp.vpr
@@ -0,0 +1,44 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method m1(s: Set[Ref])
+  requires |s| > 0
+{
+  inhale forall x: Ref :: x in (asserting(|s| > 0) in s) ==> acc(x.f)
+}
+
+method m1Fail(s: Set[Ref])
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in (asserting(|s| > 0) in s) ==> acc(x.f)
+}
+
+method m2(s: Set[Ref])
+  requires |s| > 0
+  requires !(null in s)
+{
+  inhale forall x: Ref :: x in s ==> acc((asserting (x != null) in x).f)
+}
+
+method m2Fail(s: Set[Ref])
+  requires |s| > 0
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in s ==> acc((asserting (x != null) in x).f)
+}
+
+method m3(s: Set[Ref])
+  requires |s| > 0
+  requires !(null in s)
+{
+  inhale forall x: Ref :: x in s ==> acc(x.f, asserting (x != null) in write)
+}
+
+method m3Fail(s: Set[Ref])
+  requires |s| > 0
+{
+  //:: ExpectedOutput(inhale.failed:assertion.false)
+  inhale forall x: Ref :: x in s ==> acc(x.f, asserting (x != null) in write)
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/simple-fail.vpr b/src/test/resources/all/asserting/simple-fail.vpr
new file mode 100644
index 000000000..5c5791f5d
--- /dev/null
+++ b/src/test/resources/all/asserting/simple-fail.vpr
@@ -0,0 +1,73 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method assign() {
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (false) in 0
+}
+
+method assign2(i: Int) {
+  //:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (i > 0) in 0
+}
+
+method assign3(i: Int)
+  requires i > 5
+{
+  var x: Int := asserting (i > 0) in 0
+}
+
+method pres()
+  //:: ExpectedOutput(not.wellformed:assertion.false)
+  requires asserting (false) in false
+{
+  assert false
+}
+
+method pres2(x: Ref)
+  //:: ExpectedOutput(not.wellformed:insufficient.permission)
+  requires asserting (acc(x.f)) in false
+{
+  assert false
+}
+
+method pres3(x: Ref)
+  requires acc(x.f)
+  requires asserting (acc(x.f)) in false
+{
+  assert false
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun(): Int
+{
+  asserting (false) in 0
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function fun2(x: Ref): Int
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun3(x: Ref): Int
+  requires acc(x.f)
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+function fun4(x: Ref): Int
+  requires acc(x.f) && x.f > 8
+{
+  asserting (acc(x.f) && x.f > 0) in 0
+}
+
+method stateUnchanged(x: Ref)
+  requires acc(x.f)
+{
+  var y: Int := asserting (acc(x.f)) in x.f
+  assert acc(x.f)
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/trigger.vpr b/src/test/resources/all/asserting/trigger.vpr
new file mode 100644
index 000000000..f27f14fab
--- /dev/null
+++ b/src/test/resources/all/asserting/trigger.vpr
@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function trigger(i: Int): Bool
+{
+  true
+}
+
+method triggerUse(s: Seq[Int])
+  requires |s| > 0
+  requires forall i: Int :: {trigger(i)} 0 <= i < |s| ==> s[i] > 0
+{
+  assert asserting (trigger(0)) in s[0] > 0
+}
+
+method triggerUse2(s: Seq[Int])
+  requires |s| > 0
+  requires forall i: Int :: {trigger(i)} 0 <= i < |s| ==> s[i] > 0
+{
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert s[0] > 0
+}
\ No newline at end of file
diff --git a/src/test/resources/all/asserting/wand.vpr b/src/test/resources/all/asserting/wand.vpr
new file mode 100644
index 000000000..67a026f8e
--- /dev/null
+++ b/src/test/resources/all/asserting/wand.vpr
@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+field g: Int
+
+method test0(x: Ref)
+{
+    package acc(x.f) && (asserting (acc(x.f)) in (x.f == 0)) --* acc(x.f) {}
+}
+
+method test1(x: Ref)
+{
+    //:: ExpectedOutput(package.failed:insufficient.permission)
+    package acc(x.f) && (asserting (acc(x.g)) in (x.f == 0)) --* acc(x.f) {}
+}
+

From e41821fc5c77a22edaa821ac1370a283ecd6688c Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sun, 13 Oct 2024 17:55:51 +0200
Subject: [PATCH 03/12] Test for function precondition permissions

---
 .../functions/function_precondition_perms.vpr | 242 ++++++++++++++++++
 1 file changed, 242 insertions(+)
 create mode 100644 src/test/resources/all/functions/function_precondition_perms.vpr

diff --git a/src/test/resources/all/functions/function_precondition_perms.vpr b/src/test/resources/all/functions/function_precondition_perms.vpr
new file mode 100644
index 000000000..361249984
--- /dev/null
+++ b/src/test/resources/all/functions/function_precondition_perms.vpr
@@ -0,0 +1,242 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+field g: Int
+
+predicate P(x: Ref) {
+    acc(x.f)
+}
+
+function foo(x: Ref): Int
+  requires acc(x.f)
+
+function foo2(x: Ref, b: Bool): Int
+  requires acc(x.f, b ? write : none)
+
+function foo3(x: Ref): Int
+  requires acc(x.f, wildcard)
+
+function foo4(x: Ref): Int
+  requires acc(x.f) && acc(x.f)
+
+function foo5(x: Ref): Int
+  requires forall z: Ref :: z == x ==> acc(z.f)
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function foo4p(x: Ref, y: Ref): Int
+  requires acc(x.f) && acc(y.f)
+{
+    asserting (x != y) in x.f
+}
+
+function bar(x: Ref): Int
+  requires acc(P(x), 1/4)
+{
+  unfolding acc(P(x), 1/2) in foo(x)
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function bar2(x: Ref): Int
+  requires acc(P(x), none)
+{
+  unfolding acc(P(x), 1/2) in foo(x)
+}
+
+//:: ExpectedOutput(function.not.wellformed:insufficient.permission)
+function bar3(x: Ref): Int
+  requires acc(P(x), write)
+{
+  unfolding acc(P(x), 1/2) in x.g
+}
+
+function foo6(x: Ref): Int
+  requires forall z: Ref :: false ==> acc(z.f)
+  requires acc(x.f)
+
+method test0(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo(x)
+}
+
+@exhaleMode("mce")
+method test0mce(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo(x)
+}
+
+method test0qp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, 1/2)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo(x)
+}
+
+method test1(x: Ref)
+{
+   inhale acc(x.f, none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo(x)
+}
+
+@exhaleMode("mce")
+method test1mce(x: Ref)
+{
+   inhale acc(x.f, none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo(x)
+}
+
+method test1qp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, none)
+   var tmp: Int
+   tmp := foo(x)
+}
+
+method test2(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2(x, b)
+}
+
+@exhaleMode("mce")
+method test2mce(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2(x, b)
+}
+
+method test2qp(x: Ref, b: Bool)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, b ? 1/2 : none)
+   var tmp: Int
+   tmp := foo2(x, b)
+}
+
+
+method test3(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo2(x, !b)
+}
+
+@exhaleMode("mce")
+method test3mce(x: Ref, b: Bool)
+{
+   inhale acc(x.f, b ? 1/2 : none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo2(x, !b)
+}
+
+method test3qp(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 := foo2(x, !b)
+}
+
+method test4(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo3(x)
+}
+
+@exhaleMode("mce")
+method test4mce(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo3(x)
+}
+
+method test4qp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, 1/2)
+   var tmp: Int
+   tmp := foo3(x)
+}
+
+method test4f(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo3(x)
+}
+
+@exhaleMode("mce")
+method test4mcef(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo3(x)
+}
+
+method test4qpf(x: Ref)
+{
+   inhale forall y: Ref :: false ==> acc(y.f, 1/2)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo3(x)
+}
+
+method test5(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo4(x)
+}
+
+@exhaleMode("mce")
+method test5mce(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo4(x)
+}
+
+method test5qp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(y.f, 1/2)
+   var tmp: Int
+   tmp := foo4(x)
+}
+
+method test5f(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo4(x)
+}
+
+@exhaleMode("mce")
+method test5mcef(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo4(x)
+}
+
+method test5qpf(x: Ref)
+{
+   inhale forall y: Ref :: false ==> acc(y.f, 1/2)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo4(x)
+}
+

From d6d6e65fceb454ee6c6e16c8dcbc50d70b7fd481 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sun, 13 Oct 2024 20:24:17 +0200
Subject: [PATCH 04/12] Adding and adapting tests for assert-read-only function
 preconditions

---
 .../functions/function_precondition_perms.vpr | 60 ++++++++++++++++++-
 src/test/resources/all/issues/carbon/0196.vpr | 16 ++---
 src/test/resources/all/issues/carbon/0223.vpr |  2 +-
 .../resources/all/issues/silicon/0030.vpr     | 11 +---
 .../resources/all/issues/silicon/0240.vpr     | 10 ++--
 .../resources/all/issues/silicon/0376.vpr     |  1 +
 6 files changed, 76 insertions(+), 24 deletions(-)

diff --git a/src/test/resources/all/functions/function_precondition_perms.vpr b/src/test/resources/all/functions/function_precondition_perms.vpr
index 361249984..dd8b395cd 100644
--- a/src/test/resources/all/functions/function_precondition_perms.vpr
+++ b/src/test/resources/all/functions/function_precondition_perms.vpr
@@ -24,6 +24,9 @@ function foo4(x: Ref): Int
 function foo5(x: Ref): Int
   requires forall z: Ref :: z == x ==> acc(z.f)
 
+function foo5w(x: Ref): Int
+  requires forall z: Ref :: z == x ==> acc(z.f, wildcard)
+
 //:: ExpectedOutput(function.not.wellformed:assertion.false)
 function foo4p(x: Ref, y: Ref): Int
   requires acc(x.f) && acc(y.f)
@@ -51,6 +54,14 @@ function bar3(x: Ref): Int
   unfolding acc(P(x), 1/2) in x.g
 }
 
+function bar4(x: Ref): Int
+  requires acc(P(x), 1/2) && unfolding P(x) in x.f > 0
+
+
+function bar5(x: Ref): Int
+  //:: ExpectedOutput(not.wellformed:insufficient.permission)
+  requires unfolding P(x) in x.f > 0
+
 function foo6(x: Ref): Int
   requires forall z: Ref :: false ==> acc(z.f)
   requires acc(x.f)
@@ -74,7 +85,6 @@ method test0qp(x: Ref)
 {
    inhale forall y: Ref :: y == x ==> acc(y.f, 1/2)
    var tmp: Int
-   //:: ExpectedOutput(application.precondition:insufficient.permission)
    tmp := foo(x)
 }
 
@@ -99,6 +109,7 @@ method test1qp(x: Ref)
 {
    inhale forall y: Ref :: y == x ==> acc(y.f, none)
    var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
    tmp := foo(x)
 }
 
@@ -240,3 +251,50 @@ method test5qpf(x: Ref)
    tmp := foo4(x)
 }
 
+method test6(x: Ref)
+{
+   inhale acc(x.f, 1/4)
+   assume x.f == 4
+   fold acc(P(x), 1/4)
+   var tmp: Int
+   tmp := bar4(x)
+}
+
+method test6f(x: Ref)
+{
+   inhale acc(x.f, 1/4)
+   assume x.f == -2
+   fold acc(P(x), 1/4)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:assertion.false)
+   tmp := bar4(x)
+}
+
+
+method test7(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo5(x)
+}
+
+method test7p(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:assertion.false)
+   tmp := foo5(x)
+}
+
+method test8(x: Ref)
+{
+   inhale acc(x.f, 1/2)
+   var tmp: Int
+   tmp := foo5w(x)
+}
+
+method test8p(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:assertion.false)
+   tmp := foo5w(x)
+}
\ No newline at end of file
diff --git a/src/test/resources/all/issues/carbon/0196.vpr b/src/test/resources/all/issues/carbon/0196.vpr
index fad99ad12..8aac168c3 100644
--- a/src/test/resources/all/issues/carbon/0196.vpr
+++ b/src/test/resources/all/issues/carbon/0196.vpr
@@ -33,7 +33,7 @@ method pred1(r: Ref)
     fold acc(P(r), wildcard)
     unfold acc(P(r), wildcard)
     var r2 : Ref := tester(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerFull(get(r))
 }
 
@@ -44,7 +44,7 @@ method pred2(r: Ref)
     fold acc(P(r))
     unfold acc(P(r))
     var r2 : Ref := tester(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerFull(get(r))
 }
 
@@ -55,7 +55,7 @@ method pred3(r: Ref)
     fold acc(P(r), 1/2)
     unfold acc(P(r), 1/2)
     var r2 : Ref := tester(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerFull(get(r))
 }
 
@@ -66,7 +66,7 @@ method pred4(r: Ref)
     fold acc(P2(r), wildcard)
     unfold acc(P2(r), wildcard)
     var r2 : Ref := tester(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerFull(get(r))
 }
 
@@ -77,7 +77,7 @@ method func1(r: Ref)
     fold acc(R(r), wildcard)
     unfold acc(R(r), wildcard)
     var r2 : Ref := testerfield(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerfieldFull(get(r))
 }
 
@@ -88,7 +88,7 @@ method func2(r: Ref)
     fold acc(R(r))
     unfold acc(R(r))
     var r2 : Ref := testerfield(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerfieldFull(get(r))
 }
 
@@ -99,7 +99,7 @@ method func3(r: Ref)
     fold acc(R(r), 1/2)
     unfold acc(R(r), 1/2)
     var r2 : Ref := testerfield(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerfieldFull(get(r))
 }
 
@@ -110,6 +110,6 @@ method func4(r: Ref)
     fold acc(R2(r), wildcard)
     unfold acc(R2(r), wildcard)
     var r2 : Ref := testerfield(get(r))
-    //:: ExpectedOutput(application.precondition:insufficient.permission)
+
     var r3 : Ref := testerfieldFull(get(r))
 }
diff --git a/src/test/resources/all/issues/carbon/0223.vpr b/src/test/resources/all/issues/carbon/0223.vpr
index f8a0aa193..4870d1282 100644
--- a/src/test/resources/all/issues/carbon/0223.vpr
+++ b/src/test/resources/all/issues/carbon/0223.vpr
@@ -11,7 +11,7 @@ predicate bar(x:Ref) {
 function get(x: Ref) : Int
   requires forall w:Ref :: {w in Set(x)} w in Set(x) ==> acc(bar(w))
   {
-    unfolding bar(x) in x.val
+    asserting (x in Set(x)) in unfolding bar(x) in x.val
   }
 
 method set(x:Ref, i:Int) 
diff --git a/src/test/resources/all/issues/silicon/0030.vpr b/src/test/resources/all/issues/silicon/0030.vpr
index 48c2165d6..48b05a221 100644
--- a/src/test/resources/all/issues/silicon/0030.vpr
+++ b/src/test/resources/all/issues/silicon/0030.vpr
@@ -1,12 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-function C__g(diz: Ref): Int
-   requires diz != null
-   requires acc(C__P(diz), wildcard)
-   requires acc(C__P(diz), 1 / 2)
-
-
 predicate C__P(diz: Ref)
 
 /** In Viper, exhale should proceed from left to write (earlier Carbon
@@ -16,10 +10,9 @@ Thus, exhale acc(x.f, wildcard) && acc(x.f, 1/2) is expected to fail.  */
 method C__main(diz: Ref)
    requires diz != null
    requires acc(C__P(diz), write)
-   //:: ExpectedOutput(application.precondition:insufficient.permission)
-   requires C__g(diz) > 0
 {
-
+   //:: ExpectedOutput(exhale.failed:insufficient.permission)
+   exhale acc(C__P(diz), wildcard) && acc(C__P(diz), 1 / 2)
 }
 
 method test(diz:Ref)
diff --git a/src/test/resources/all/issues/silicon/0240.vpr b/src/test/resources/all/issues/silicon/0240.vpr
index 3b2ef394d..b258a614b 100644
--- a/src/test/resources/all/issues/silicon/0240.vpr
+++ b/src/test/resources/all/issues/silicon/0240.vpr
@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
  field next: Ref
  field data: Int
 
@@ -54,7 +54,7 @@ method test04a(this: Ref)
 method test04b(this: Ref)
   requires acc(bla(this), 1/2)
 {
-  //:: ExpectedOutput(application.precondition:insufficient.permission)
+
   assert unfolding acc(bla(this), 1/2) in foo(this)
 }
 
@@ -98,6 +98,6 @@ method test04a_qp(xs: Set[Ref])
 method test04b_qp(xs: Set[Ref])
   requires acc(bla_qp(xs), 1/2)
 {
-  //:: ExpectedOutput(application.precondition:insufficient.permission)
+
   assert unfolding acc(bla_qp(xs), 1/2) in foo_qp(xs)
 }
diff --git a/src/test/resources/all/issues/silicon/0376.vpr b/src/test/resources/all/issues/silicon/0376.vpr
index 29d1c0842..9fed00943 100644
--- a/src/test/resources/all/issues/silicon/0376.vpr
+++ b/src/test/resources/all/issues/silicon/0376.vpr
@@ -23,6 +23,7 @@ field f: Int
 
 function foo(x: Ref): Int
   requires acc(x.f) && acc(x.f)
+  //:: ExpectedOutput(postcondition.violated:assertion.false)
   ensures false
 { x.f }
 

From 4ea735d6fdb47570d8b2105d9f051e76570f7b9d Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sun, 13 Oct 2024 21:32:09 +0200
Subject: [PATCH 05/12] Warnings when using specific permission amounts in
 functions that will be ignored

---
 src/main/scala/viper/silver/ast/Program.scala   |  3 ++-
 .../viper/silver/ast/utility/Consistency.scala  | 17 +++++++++++++++++
 .../viper/silver/frontend/SilFrontend.scala     |  7 +++++--
 .../scala/viper/silver/reporter/Message.scala   |  5 +++++
 .../scala/viper/silver/reporter/Reporter.scala  |  7 +++++++
 .../silver/verifier/VerificationResult.scala    |  4 ++--
 6 files changed, 38 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index 1ea501bef..e8c3227ff 100644
--- a/src/main/scala/viper/silver/ast/Program.scala
+++ b/src/main/scala/viper/silver/ast/Program.scala
@@ -471,7 +471,8 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres
         }).execute[Node](pre)
       })
       errors
-    }
+    } ++
+    Consistency.warnAboutFunctionPermissionAmounts(this)
 
   val scopedDecls: Seq[Declaration] = formalArgs
   /**
diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala
index cb68e36c4..da06ed6f8 100644
--- a/src/main/scala/viper/silver/ast/utility/Consistency.scala
+++ b/src/main/scala/viper/silver/ast/utility/Consistency.scala
@@ -184,6 +184,23 @@ object Consistency {
     (if(!noResult(e)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", e.pos)) else Seq())
   }
 
+  def warnAboutFunctionPermissionAmounts(f: Function): Seq[ConsistencyError] = {
+    def hasSpecificPermAmounts(e: Exp): Boolean = e match {
+      case CondExp(_, thn, els) => hasSpecificPermAmounts(thn) || hasSpecificPermAmounts(els)
+      case _: FractionalPerm => true
+      case _ => false
+    }
+    val preWarnings = f.pres.collect(pre => pre.collect{
+      case ap: AccessPredicate if hasSpecificPermAmounts(ap.perm) =>
+        ConsistencyError("Function precondition contains specific permission amount that will be treated like write/wildcard.", ap.pos, false)
+    }).flatten
+    val bodyWarnings = f.body.toSeq.map(body => body.collect{
+      case ap: AccessPredicate if hasSpecificPermAmounts(ap.perm) =>
+        ConsistencyError("Function body contains specific permission amount that will be treated like write/wildcard.", ap.pos, false)
+    }).flatten
+    preWarnings ++ bodyWarnings
+  }
+
   /** Check all properties required for a contract expression that is not a postcondition (precondition, invariant, predicate) */
   def checkNonPostContract(e: Exp) : Seq[ConsistencyError]  = {
     (if(!(e isSubtype Bool)) Seq(ConsistencyError(s"Contract $e: ${e.typ} must be boolean.", e.pos)) else Seq()) ++
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index caf49316f..ef779af25 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -377,9 +377,12 @@ trait SilFrontend extends DefaultFrontend {
     var errors = input.checkTransitively
     if (backendTypeFormat.isDefined)
       errors = errors ++ Consistency.checkBackendTypes(input, backendTypeFormat.get)
-    if (errors.isEmpty) {
+    val (actualErrors, warnings) = errors partition (_.isError)
+    if (warnings.nonEmpty)
+      reporter.report(ConsistencyWarnings(warnings))
+    if (actualErrors.isEmpty) {
       Succ(input)
     } else
-      Fail(errors)
+      Fail(actualErrors)
   }
 }
diff --git a/src/main/scala/viper/silver/reporter/Message.scala b/src/main/scala/viper/silver/reporter/Message.scala
index 441810eee..d4479eef2 100644
--- a/src/main/scala/viper/silver/reporter/Message.scala
+++ b/src/main/scala/viper/silver/reporter/Message.scala
@@ -269,6 +269,11 @@ case class WarningsDuringTypechecking(warnings: Seq[TypecheckerWarning]) extends
   override val name: String = "warnings_during_typechecking"
 }
 
+case class ConsistencyWarnings(warnings: Seq[ConsistencyError]) extends Message {
+  override lazy val toString: String = s"consistency_warnings(warnings=${warnings.toString})"
+  override val name: String = "consistency_warnings"
+}
+
 case class WarningsDuringVerification(warnings: Seq[VerifierWarning]) extends Message {
   override lazy val toString: String = s"warnings_during_verification(warnings=${warnings.toString})"
   override val name: String = "warnings_during_verification"
diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala
index 0c51bd50d..8f013e178 100644
--- a/src/main/scala/viper/silver/reporter/Reporter.scala
+++ b/src/main/scala/viper/silver/reporter/Reporter.scala
@@ -56,6 +56,10 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
         warnings.foreach(report => {
           csv_file.write(s"WarningsDuringVerification,${report}\n")
         })
+      case ConsistencyWarnings(warnings) =>
+        warnings.foreach(report => {
+          csv_file.write(s"ConsistencyWarnings,${report}\n")
+        })
       case InvalidArgumentsReport(_, errors) =>
         errors.foreach(error => {
           csv_file.write(s"WarningsDuringParsing,${error}\n")
@@ -150,6 +154,9 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
       case WarningsDuringVerification(warnings) =>
         warnings.foreach(println)
 
+      case ConsistencyWarnings(warnings) =>
+        warnings.foreach(println)
+
       case AnnotationWarning(text) =>
         println(s"Annotation warning: ${text}")
 
diff --git a/src/main/scala/viper/silver/verifier/VerificationResult.scala b/src/main/scala/viper/silver/verifier/VerificationResult.scala
index 95980f6c5..8631b8690 100644
--- a/src/main/scala/viper/silver/verifier/VerificationResult.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationResult.scala
@@ -106,9 +106,9 @@ case class VerifierWarning(message: String, override val pos: Position)
 }
 
 /** An error during consistency-checking an AST node */
-case class ConsistencyError(message: String, pos:Position) extends AbstractError {
+case class ConsistencyError(message: String, pos:Position, isError: Boolean = true) extends AbstractError {
   def fullId = "consistency.error"
-  def readableMessage: String = s"Consistency error: $message ($pos)"
+  def readableMessage: String = s"Consistency ${if (isError) "error" else "warning"}: $message ($pos)"
 }
 
 /** A typechecker error. */

From 89dce6fde51d0a9bebf6db83c8968a5778be5a1f Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sun, 13 Oct 2024 21:58:04 +0200
Subject: [PATCH 06/12] Fixed test annotations

---
 .../resources/all/functions/function_precondition_perms.vpr   | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/test/resources/all/functions/function_precondition_perms.vpr b/src/test/resources/all/functions/function_precondition_perms.vpr
index dd8b395cd..bab3cbb3f 100644
--- a/src/test/resources/all/functions/function_precondition_perms.vpr
+++ b/src/test/resources/all/functions/function_precondition_perms.vpr
@@ -281,7 +281,7 @@ method test7(x: Ref)
 method test7p(x: Ref)
 {
    var tmp: Int
-   //:: ExpectedOutput(application.precondition:assertion.false)
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
    tmp := foo5(x)
 }
 
@@ -295,6 +295,6 @@ method test8(x: Ref)
 method test8p(x: Ref)
 {
    var tmp: Int
-   //:: ExpectedOutput(application.precondition:assertion.false)
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
    tmp := foo5w(x)
 }
\ No newline at end of file

From a0fbf3aa6f1d375e2f59a6c350d696856ec7dc5e Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 15 Oct 2024 15:14:17 +0200
Subject: [PATCH 07/12] Also test all important scenarios for predicates, make
 sure non-aliasing is still assumed outside functions

---
 .../functions/function_precondition_perms.vpr | 99 ++++++++++++++++++-
 1 file changed, 96 insertions(+), 3 deletions(-)

diff --git a/src/test/resources/all/functions/function_precondition_perms.vpr b/src/test/resources/all/functions/function_precondition_perms.vpr
index bab3cbb3f..84a8feac2 100644
--- a/src/test/resources/all/functions/function_precondition_perms.vpr
+++ b/src/test/resources/all/functions/function_precondition_perms.vpr
@@ -12,6 +12,9 @@ predicate P(x: Ref) {
 function foo(x: Ref): Int
   requires acc(x.f)
 
+function foop(x: Ref): Int
+  requires P(x)
+
 function foo2(x: Ref, b: Bool): Int
   requires acc(x.f, b ? write : none)
 
@@ -27,13 +30,28 @@ function foo5(x: Ref): Int
 function foo5w(x: Ref): Int
   requires forall z: Ref :: z == x ==> acc(z.f, wildcard)
 
+function foo5p(x: Ref): Int
+  requires forall z: Ref :: z == x ==> P(z)
+
+function foo5pw(x: Ref): Int
+  requires forall z: Ref :: z == x ==> acc(P(z), wildcard)
+
 //:: ExpectedOutput(function.not.wellformed:assertion.false)
-function foo4p(x: Ref, y: Ref): Int
+function nonAliasF(x: Ref, y: Ref): Int
   requires acc(x.f) && acc(y.f)
 {
     asserting (x != y) in x.f
 }
 
+predicate nonAliasPred(x: Ref, y: Ref) {
+    acc(x.f) && acc(y.f) && asserting (x != y) in true
+}
+
+method nonAliasM(x: Ref, y: Ref) {
+    inhale acc(x.f) && acc(y.f)
+    assert x != y
+}
+
 function bar(x: Ref): Int
   requires acc(P(x), 1/4)
 {
@@ -88,6 +106,28 @@ method test0qp(x: Ref)
    tmp := foo(x)
 }
 
+method test0p(x: Ref)
+{
+   inhale acc(P(x), 1/2)
+   var tmp: Int
+   tmp := foop(x)
+}
+
+@exhaleMode("mce")
+method test0pmce(x: Ref)
+{
+   inhale acc(P(x), 1/2)
+   var tmp: Int
+   tmp := foop(x)
+}
+
+method test0pqp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(P(y), 1/2)
+   var tmp: Int
+   tmp := foop(x)
+}
+
 method test1(x: Ref)
 {
    inhale acc(x.f, none)
@@ -113,6 +153,31 @@ method test1qp(x: Ref)
    tmp := foo(x)
 }
 
+method test1p(x: Ref)
+{
+   inhale acc(P(x), none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foop(x)
+}
+
+@exhaleMode("mce")
+method test1pmce(x: Ref)
+{
+   inhale acc(P(x), none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foop(x)
+}
+
+method test1pqp(x: Ref)
+{
+   inhale forall y: Ref :: y == x ==> acc(P(y), none)
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foop(x)
+}
+
 method test2(x: Ref, b: Bool)
 {
    inhale acc(x.f, b ? 1/2 : none)
@@ -278,13 +343,27 @@ method test7(x: Ref)
    tmp := foo5(x)
 }
 
-method test7p(x: Ref)
+method test7f(x: Ref)
 {
    var tmp: Int
    //:: ExpectedOutput(application.precondition:insufficient.permission)
    tmp := foo5(x)
 }
 
+method test7p(x: Ref)
+{
+   inhale acc(P(x), 1/2)
+   var tmp: Int
+   tmp := foo5p(x)
+}
+
+method test7pf(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo5p(x)
+}
+
 method test8(x: Ref)
 {
    inhale acc(x.f, 1/2)
@@ -292,9 +371,23 @@ method test8(x: Ref)
    tmp := foo5w(x)
 }
 
-method test8p(x: Ref)
+method test8f(x: Ref)
 {
    var tmp: Int
    //:: ExpectedOutput(application.precondition:insufficient.permission)
    tmp := foo5w(x)
+}
+
+method test8p(x: Ref)
+{
+   inhale acc(P(x), 1/2)
+   var tmp: Int
+   tmp := foo5pw(x)
+}
+
+method test8pf(x: Ref)
+{
+   var tmp: Int
+   //:: ExpectedOutput(application.precondition:insufficient.permission)
+   tmp := foo5pw(x)
 }
\ No newline at end of file

From 626437b04aaa354061246f8d07831ad8effdeb93 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 15 Oct 2024 15:28:34 +0200
Subject: [PATCH 08/12] Add option to enable old behavior (respect function pre
 permission amounts)

---
 .../scala/viper/silver/frontend/SilFrontEndConfig.scala    | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
index 69820bc6c..1ddcf82df 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
@@ -139,6 +139,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = false
   )
 
+  val respectFunctionPrecPermAmounts = opt[Boolean]("respectFunctionPrecPermAmounts",
+    descr = "Respects precise permission amounts in function preconditions instead of only checking read access.",
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
   val submitForEvaluation = opt[Boolean](name = "submitForEvaluation",
     descr = "Whether to allow storing the current program for future evaluation.",
     default = Some(false),

From 4509152c35ae7ceda9441c47dcc25cce962d47c0 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 22 Oct 2024 14:34:18 +0200
Subject: [PATCH 09/12] Making permission amounts in access predicates optional

---
 .../scala/viper/silver/ast/Expression.scala   |  6 ++++--
 .../silver/ast/utility/Expressions.scala      |  2 +-
 .../silver/ast/utility/InverseFunctions.scala |  6 +++---
 .../viper/silver/ast/utility/Nodes.scala      |  2 +-
 .../silver/ast/utility/Permissions.scala      | 21 +++++++++++++------
 .../scala/viper/silver/parser/ParseAst.scala  |  3 ++-
 .../viper/silver/parser/Translator.scala      |  5 ++---
 .../PredicateInstancePlugin.scala             |  2 +-
 .../silver/testing/BackendTypeTest.scala      |  8 +++----
 src/test/scala/ChopperTests.scala             |  2 +-
 src/test/scala/ConsistencyTests.scala         |  8 +++----
 src/test/scala/FeatureCombinationsTests.scala |  8 +++----
 src/test/scala/MethodDependencyTests.scala    | 10 ++++-----
 src/test/scala/SimplifierTests.scala          |  2 +-
 src/test/scala/UtilityTests.scala             |  2 +-
 15 files changed, 49 insertions(+), 38 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 0d206d9ae..1964f339f 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -285,14 +285,16 @@ object AccessPredicate {
 }
 
 /** An accessibility predicate for a field location. */
-case class FieldAccessPredicate(loc: FieldAccess, perm: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+case class FieldAccessPredicate(loc: FieldAccess, permExp: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+  val perm = permExp.getOrElse(FullPerm()(pos, NoInfo, NoTrafos))
   override lazy val check : Seq[ConsistencyError] =
     (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq()) ++ Consistency.checkWildcardUsage(perm)
   val typ: Bool.type = Bool
 }
 
 /** An accessibility predicate for a predicate location. */
-case class PredicateAccessPredicate(loc: PredicateAccess, perm: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+case class PredicateAccessPredicate(loc: PredicateAccess, permExp: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
+  val perm = permExp.getOrElse(FullPerm()(pos, NoInfo, NoTrafos))
   override lazy val check : Seq[ConsistencyError] =
     (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq()) ++ Consistency.checkWildcardUsage(perm)
   val typ: Bool.type = Bool
diff --git a/src/main/scala/viper/silver/ast/utility/Expressions.scala b/src/main/scala/viper/silver/ast/utility/Expressions.scala
index b4fa7c980..318ea49fc 100644
--- a/src/main/scala/viper/silver/ast/utility/Expressions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Expressions.scala
@@ -191,7 +191,7 @@ object Expressions {
         }
         // Conditions for the current node.
         val conds: Seq[Exp] = n match {
-          case f@FieldAccess(rcv, _) => List(NeCmp(rcv, NullLit()(p))(p), FieldAccessPredicate(f, WildcardPerm()(p))(p))
+          case f@FieldAccess(rcv, _) => List(NeCmp(rcv, NullLit()(p))(p), FieldAccessPredicate(f, Some(WildcardPerm()(p)))(p))
           case f: FuncApp => prog.findFunction(f.funcname).pres
           case Div(_, q) => List(NeCmp(q, IntLit(0)(p))(p))
           case Mod(_, q) => List(NeCmp(q, IntLit(0)(p))(p))
diff --git a/src/main/scala/viper/silver/ast/utility/InverseFunctions.scala b/src/main/scala/viper/silver/ast/utility/InverseFunctions.scala
index e8ebe3e36..b778f8464 100644
--- a/src/main/scala/viper/silver/ast/utility/InverseFunctions.scala
+++ b/src/main/scala/viper/silver/ast/utility/InverseFunctions.scala
@@ -37,11 +37,11 @@ object InverseFunctions {
             val axiom1 = Forall(qvars, forall.triggers, Implies(cond, equalities)(pos, info, errT))(pos, info, errT)
             var condReplaced = cond
             var rcvReplaced = fap.loc.rcv
-            var permReplaced = fap.perm
+            var permReplaced = fap.permExp
             for (i <- 0 until qvars.length){
               condReplaced = condReplaced.replace(qvars(i).localVar, invsOfR(i))
               rcvReplaced = rcvReplaced.replace(qvars(i).localVar, invsOfR(i))
-              permReplaced = permReplaced.replace(qvars(i).localVar, invsOfR(i))
+              permReplaced = permReplaced.map(_.replace(qvars(i).localVar, invsOfR(i)))
             }
             val axiom2 = Forall(Seq(r), Seq(Trigger(invsOfR)(pos, info, errT)), Implies(condReplaced, EqCmp(rcvReplaced, r.localVar)(pos, info, errT))(pos, info, errT))(pos, info, errT)
             val acc1 = FieldAccessPredicate(FieldAccess(r.localVar, fap.loc.field)(), permReplaced)()
@@ -65,7 +65,7 @@ object InverseFunctions {
             val axiom2 = Forall(formalArgs, Seq(Trigger(invsOfFormalArgs)(pos, info, errT)), Implies(cond.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap), invArgsConj)(pos, info, errT))(pos, info, errT)
 
             val cond1 = cond.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap)
-            val acc1 = PredicateAccessPredicate(PredicateAccess(formalArgs map (_.localVar), pred.name)(pos, info, errT), pap.perm.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap))(pos, info, errT)
+            val acc1 = PredicateAccessPredicate(PredicateAccess(formalArgs map (_.localVar), pred.name)(pos, info, errT), pap.permExp.map(_.replace((qvars map (_.localVar) zip invsOfFormalArgs).toMap)))(pos, info, errT)
             val forall1 = Forall(formalArgs, Seq(Trigger(invsOfFormalArgs)(pos, info, errT)), Implies(cond1, acc1)(pos, info, errT))(pos, info, errT)
 
             val domain = Domain(domName, invs, Seq())(pos, info, errT)
diff --git a/src/main/scala/viper/silver/ast/utility/Nodes.scala b/src/main/scala/viper/silver/ast/utility/Nodes.scala
index 0dc99d7dd..d7d568fef 100644
--- a/src/main/scala/viper/silver/ast/utility/Nodes.scala
+++ b/src/main/scala/viper/silver/ast/utility/Nodes.scala
@@ -80,7 +80,7 @@ object Nodes {
           case _: AbstractLocalVar => Nil
           case FieldAccess(rcv, _) => Seq(rcv)
           case PredicateAccess(params, _) => params
-          case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc, perm)
+          case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc) ++ perm.toSeq
           case Unfolding(acc, body) => Seq(acc, body)
           case Applying(wand, body) => Seq(wand, body)
           case Old(exp) => Seq(exp)
diff --git a/src/main/scala/viper/silver/ast/utility/Permissions.scala b/src/main/scala/viper/silver/ast/utility/Permissions.scala
index 858756002..bf4caee5a 100644
--- a/src/main/scala/viper/silver/ast/utility/Permissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Permissions.scala
@@ -31,12 +31,21 @@ object Permissions {
            "Internal error: attempted to permission-scale expression " + e.toString +
                " by non-permission-typed expression " + permFactor.toString)
 
-    if(permFactor.isInstanceOf[FullPerm])
+    def multiplyPermOpt(op: Option[Exp]): Option[Exp] = op match {
+      case Some(p) => Some(PermMul(p, permFactor)(p.pos, p.info))
+      case None => Some(permFactor)
+    }
+
+    if (permFactor.isInstanceOf[FullPerm]) {
       e
-    else
-      e.transform({
-        case fa@FieldAccessPredicate(loc,p) => FieldAccessPredicate(loc,PermMul(p,permFactor)(p.pos,p.info))(fa.pos,fa.info)
-        case pa@PredicateAccessPredicate(loc,p) => PredicateAccessPredicate(loc,PermMul(p,permFactor)(p.pos,p.info))(pa.pos,pa.info)
+    } else {
+      e.transform{
+        case fa@FieldAccessPredicate(loc, p) =>
+          FieldAccessPredicate(loc, multiplyPermOpt(p))(fa.pos, fa.info)
+        case pa@PredicateAccessPredicate(loc, p) =>
+          PredicateAccessPredicate(loc, multiplyPermOpt(p))(pa.pos, pa.info)
         case _: MagicWand => sys.error("Cannot yet permission-scale magic wands")
-      })}
+      }
+    }
+  }
 }
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 4e59f54c4..4a5509d49 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1198,7 +1198,8 @@ case class PAccPred(op: PKwOp.Acc, amount: PGrouped.Paren[PMaybePairArgument[PLo
     Map(POpApp.pArgS(1) -> Perm, POpApp.pResS -> Impure),
   )
   def loc = amount.inner.first
-  def perm = amount.inner.second.map(_._2).getOrElse(PFullPerm.implied())
+  def perm = permExp.getOrElse(PFullPerm.implied())
+  def permExp: Option[PExp] = amount.inner.second.map(_._2)
   override val args = Seq(loc, perm)
 }
 
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 4a6f469d2..600cbf6fa 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -504,8 +504,7 @@ case class Translator(program: PProgram) {
             }
           case _: Predicate =>
             val inner = PredicateAccess(args.inner.toSeq map exp, findPredicate(func).name) (pos, info)
-            val fullPerm = FullPerm()(pos, info)
-            PredicateAccessPredicate(inner, fullPerm) (pos, info)
+            PredicateAccessPredicate(inner, None) (pos, info)
           case _ => sys.error("unexpected reference to non-function")
         }
       case PNewExp(_, _) => sys.error("unexpected `new` expression")
@@ -568,7 +567,7 @@ case class Translator(program: PProgram) {
       case PEpsilon(_) =>
         EpsilonPerm()(pos, info)
       case acc: PAccPred =>
-        val p = exp(acc.perm)
+        val p = acc.permExp.map(exp)
         exp(acc.loc) match {
           case loc@FieldAccess(_, _) =>
             FieldAccessPredicate(loc, p)(pos, info)
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
index b8816e3b0..450f72ff5 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
@@ -68,7 +68,7 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
             Function(piFunctionName,
               pred.formalArgs,
               DomainType(PredicateInstanceDomain.get, Map()),
-              Seq(PredicateAccessPredicate(PredicateAccess(pred.formalArgs.map(_.localVar), pred.name)(), WildcardPerm()())(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)),
+              Seq(PredicateAccessPredicate(PredicateAccess(pred.formalArgs.map(_.localVar), pred.name)(), Some(WildcardPerm()()))(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)),
               Seq(),
               None
             )(PredicateInstanceDomain.get.pos, PredicateInstanceDomain.get.info)
diff --git a/src/main/scala/viper/silver/testing/BackendTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
index 0f973825d..3b070fe09 100644
--- a/src/main/scala/viper/silver/testing/BackendTypeTest.scala
+++ b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
@@ -33,7 +33,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val p2_decl = LocalVarDecl("lol", SetType(t))()
     val p2_ref= p2_decl.localVar
     val fieldAcc = FieldAccess(p1_ref, field)()
-    val perm = FieldAccessPredicate(fieldAcc, FullPerm()())()
+    val perm = FieldAccessPredicate(fieldAcc, Some(FullPerm()()))()
     val element_in_param = AnySetContains(fieldAcc, p2_ref)()
 
     val getPerm = Inhale(perm)()
@@ -51,7 +51,7 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val setParam = LocalVarDecl("refs", SetType(Ref))()
     val floatParam = LocalVarDecl("val", fp.typ)()
     val x = LocalVarDecl("x", Ref)()
-    val qpBody = Implies(AnySetContains(x.localVar, setParam.localVar)(), FieldAccessPredicate(FieldAccess(x.localVar, fld)(), FullPerm()())())()
+    val qpBody = Implies(AnySetContains(x.localVar, setParam.localVar)(), FieldAccessPredicate(FieldAccess(x.localVar, fld)(), None)())()
     val qp = Forall(Seq(x), Seq(), qpBody)()
     val inhaleQp = Inhale(qp)()
     val fieldInfoBody = Implies(AnySetContains(x.localVar, setParam.localVar)(), NeCmp(FieldAccess(x.localVar, fld)(), floatParam.localVar)())()
@@ -151,14 +151,14 @@ trait BackendTypeTest extends AnyFunSuite with Matchers with BeforeAndAfterAllCo
     val field = Field("val_float", fp.typ)()
     val selfVar = LocalVarDecl("self", Ref)()
     val fieldAcc = FieldAccess(selfVar.localVar, field)()
-    val fieldAccPred = FieldAccessPredicate(fieldAcc, FullPerm()())()
+    val fieldAccPred = FieldAccessPredicate(fieldAcc, Some(FullPerm()()))()
     val pred = Predicate("f64", Seq(selfVar), Some(fieldAccPred))()
 
     val inhale = Inhale(fieldAccPred)()
     val fpVal = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(value)()))()))()
     val assign = FieldAssign(fieldAcc, fpVal)()
     val predAcc = PredicateAccess(Seq(selfVar.localVar), pred.name)()
-    val predAccPred = PredicateAccessPredicate(predAcc, FullPerm()())()
+    val predAccPred = PredicateAccessPredicate(predAcc, None)()
     val fold = Fold(predAccPred)()
     val exhale = Exhale(predAccPred)()
 
diff --git a/src/test/scala/ChopperTests.scala b/src/test/scala/ChopperTests.scala
index f954432c6..a20742ae8 100644
--- a/src/test/scala/ChopperTests.scala
+++ b/src/test/scala/ChopperTests.scala
@@ -223,7 +223,7 @@ class ChopperTests extends AnyFunSuite with Matchers with Inside {
     val callee = calleeStub.copy(body = Some(ast.TrueLit()()))(ast.NoPosition, ast.NoInfo, ast.NoTrafos)
     val call = ast.PredicateAccess(Seq.empty, predicateName = callee.name)()
     val caller1 = callerStub1.copy(body = Some(call))(ast.NoPosition, ast.NoInfo, ast.NoTrafos)
-    val unfolding = ast.Unfolding(ast.PredicateAccessPredicate(call, ast.FullPerm()())(), ast.TrueLit()())()
+    val unfolding = ast.Unfolding(ast.PredicateAccessPredicate(call, None)(), ast.TrueLit()())()
     val caller2 = callerStub2.copy(body = Some(unfolding))(ast.NoPosition, ast.NoInfo, ast.NoTrafos)
 
     val program = ast.Program(Seq.empty, Seq.empty, Seq.empty, Seq(callee, caller1, caller2), Seq.empty, Seq.empty)()
diff --git a/src/test/scala/ConsistencyTests.scala b/src/test/scala/ConsistencyTests.scala
index 3def23bdd..a44505272 100644
--- a/src/test/scala/ConsistencyTests.scala
+++ b/src/test/scala/ConsistencyTests.scala
@@ -157,11 +157,11 @@ class ConsistencyTests extends AnyFunSuite with Matchers {
     val callerPosts =
       Seq(
         // Wrong: zero arguments
-        PredicateAccessPredicate(PredicateAccess(Seq(), "P")(), FullPerm()())(),
+        PredicateAccessPredicate(PredicateAccess(Seq(), "P")(), Some(FullPerm()()))(),
         // Wrong: wrong argument type
-        PredicateAccessPredicate(PredicateAccess(Seq(callerBoolVar), "P")(), FullPerm()())(),
+        PredicateAccessPredicate(PredicateAccess(Seq(callerBoolVar), "P")(), None)(),
         // Correct
-        PredicateAccessPredicate(PredicateAccess(Seq(callerIntVar), "P")(), FullPerm()())()
+        PredicateAccessPredicate(PredicateAccess(Seq(callerIntVar), "P")(), None)()
       )
 
     val caller =
@@ -250,7 +250,7 @@ class ConsistencyTests extends AnyFunSuite with Matchers {
   test("Testing if Forall AST nodes have implication as expression") {
 
     val f = Field("f", Int)()
-    val forall = Forall(Seq(LocalVarDecl("i", Int)()), Seq(), CondExp(FalseLit()(), TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("r", Ref)(), f)(), FullPerm()())())())()
+    val forall = Forall(Seq(LocalVarDecl("i", Int)()), Seq(), CondExp(FalseLit()(), TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("r", Ref)(), f)(), Some(FullPerm()()))())())()
 
     forall.checkTransitively shouldBe Seq(
       ConsistencyError("Quantified permissions must have an implication as expression, with the access predicate in its right-hand side.", NoPosition)
diff --git a/src/test/scala/FeatureCombinationsTests.scala b/src/test/scala/FeatureCombinationsTests.scala
index a2164a5bf..e1951c84e 100644
--- a/src/test/scala/FeatureCombinationsTests.scala
+++ b/src/test/scala/FeatureCombinationsTests.scala
@@ -30,7 +30,7 @@ class FeatureCombinationsTests extends AnyFunSuite with Matchers {
   }
 
   test("Forall of the Quantified Permissions form") {
-    val q0 = Forall( Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), FullPerm()())() )() )()
+    val q0 = Forall( Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), None)() )() )()
 
     assert(q0.isValid)
   }
@@ -46,7 +46,7 @@ class FeatureCombinationsTests extends AnyFunSuite with Matchers {
   test("Forall with predicate application in body expression") {
     val pred = PredicateAccess(Seq(LocalVar("x", Ref)()), "pred")(NoPosition, NoInfo, NoTrafos)
     val perm = FullPerm()()
-    val q1 = Forall(Seq(LocalVarDecl("i", Int)()), Seq(), PredicateAccessPredicate(pred, perm)())()
+    val q1 = Forall(Seq(LocalVarDecl("i", Int)()), Seq(), PredicateAccessPredicate(pred, Some(perm))())()
 
     assert(!q1.isValid)
   }
@@ -103,8 +103,8 @@ class FeatureCombinationsTests extends AnyFunSuite with Matchers {
   }
 
   test("Magic wand with Quantified Permissions") {
-    val wand1 = MagicWand(TrueLit()(), Forall(Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), FullPerm()())())() )())()
-    val wand2 = MagicWand(Forall(Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), FullPerm()())())() )(), TrueLit()())()
+    val wand1 = MagicWand(TrueLit()(), Forall(Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), None)())() )())()
+    val wand2 = MagicWand(Forall(Seq(LocalVarDecl("x", Ref)()), Seq(), Implies(TrueLit()(), FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("a", Int)())(), Some(FullPerm()()))())() )(), TrueLit()())()
 
     assert(!wand1.isValid)
     assert(!wand2.isValid)
diff --git a/src/test/scala/MethodDependencyTests.scala b/src/test/scala/MethodDependencyTests.scala
index 497c7fc66..d9639433e 100644
--- a/src/test/scala/MethodDependencyTests.scala
+++ b/src/test/scala/MethodDependencyTests.scala
@@ -94,24 +94,24 @@ class MethodDependencyTests extends AnyFunSuite with Matchers {
   val fun1: Function = Function("fun1", Seq(), Bool, Seq(), Seq(), None)()
   val fun2: Function = Function("fun2", Seq(), Bool, Seq(), Seq(), None)()
   val fun3: Function = Function("fun3", Seq(), Bool, Seq(), Seq(), None)()
-  val fun4: Function = Function("fun4", Seq(LocalVarDecl("x", Ref)()), Bool, Seq(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("f4", Bool)())(),FullPerm()())()), Seq(), None)()
+  val fun4: Function = Function("fun4", Seq(LocalVarDecl("x", Ref)()), Bool, Seq(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), Field("f4", Bool)())(), None)()), Seq(), None)()
   val p0: Predicate = Predicate("p0", Seq(), None)()
   val p1: Predicate = Predicate("p1", Seq(), None)()
   val p2: Predicate = Predicate("p2", Seq(), None)()
   val p3: Predicate = Predicate("p3", Seq(), None)()
   val p4: Predicate = Predicate("p4", Seq(LocalVarDecl("x", Ref)()), Some(FuncApp(fun4, Seq(LocalVar("x", Ref)()))()))()
   val m1: Method = Method("m1", Seq(), Seq(), Seq(), Seq(), Some(Seqn(Seq(), Seq())()))()
-  val m0: Method = Method("m0", Seq(LocalVarDecl("x", Ref)()), Seq(), Seq(PredicateAccessPredicate(PredicateAccess(Seq(LocalVar("x", Ref)()), p4.name)(), FullPerm()())()), Seq(), Some(Seqn(Seq(MethodCall(m1,Seq(),Seq())()), Seq())()))()
+  val m0: Method = Method("m0", Seq(LocalVarDecl("x", Ref)()), Seq(), Seq(PredicateAccessPredicate(PredicateAccess(Seq(LocalVar("x", Ref)()), p4.name)(), Some(FullPerm()()))()), Seq(), Some(Seqn(Seq(MethodCall(m1,Seq(),Seq())()), Seq())()))()
   val test: Method = Method("test",
     Seq(LocalVarDecl("x", Ref)()),
     Seq(),
     // preconditions:
-    Seq(And(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), f0)(), FullPerm()())(), And(FuncApp(fun0, Seq())(), PredicateAccessPredicate(PredicateAccess(Seq(), p0.name)(), FullPerm()())())())()),
+    Seq(And(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), f0)(), None)(), And(FuncApp(fun0, Seq())(), PredicateAccessPredicate(PredicateAccess(Seq(), p0.name)(), Some(FullPerm()()))())())()),
     // postconditions:
-    Seq(And(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), f1)(), FullPerm()())(), And(FuncApp(fun1, Seq())(), PredicateAccessPredicate(PredicateAccess(Seq(), p1.name)(), FullPerm()())())())()),
+    Seq(And(FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(), f1)(), Some(FullPerm()()))(), And(FuncApp(fun1, Seq())(), PredicateAccessPredicate(PredicateAccess(Seq(), p1.name)(), None)())())()),
     // body of the method:
     Some(Seqn(Seq(
-      Unfold(PredicateAccessPredicate(PredicateAccess(Seq(), p2.name)(), FullPerm()())())(),
+      Unfold(PredicateAccessPredicate(PredicateAccess(Seq(), p2.name)(), None)())(),
       While(TrueLit()(), Seq(FieldAccess(LocalVar("x", Ref)(), f2)()), Seqn(Seq(
         // body of the outer loop
         While(TrueLit()(), Seq(FuncApp(fun2, Seq())()), Seqn(Seq(
diff --git a/src/test/scala/SimplifierTests.scala b/src/test/scala/SimplifierTests.scala
index 896862a9a..a6bbec1d0 100644
--- a/src/test/scala/SimplifierTests.scala
+++ b/src/test/scala/SimplifierTests.scala
@@ -19,7 +19,7 @@ class SimplifierTests extends AnyFunSuite with Matchers {
     val b = LocalVar("a", Bool)()
     val acc = PredicateAccessPredicate(
       PredicateAccess(Nil, "pred")(),
-      FullPerm()()
+      None
     )()
     val tru = TrueLit()()
 
diff --git a/src/test/scala/UtilityTests.scala b/src/test/scala/UtilityTests.scala
index 950723562..c98e62f92 100644
--- a/src/test/scala/UtilityTests.scala
+++ b/src/test/scala/UtilityTests.scala
@@ -15,7 +15,7 @@ class UtilityTests extends AnyFunSuite with Matchers {
   /* These tests exercise utility methods on the AST (transformers, visitors, rewriters etc.) */
 
   test("Assume rewriter (direct)"){ // assume acc(x.f) -> rewritten to -> assume perm(x.f) >= write
-    val assumeBody = FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(),Field("f",Int)(NoPosition))(NoPosition), FullPerm()(NoPosition))(NoPosition)
+    val assumeBody = FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(),Field("f",Int)(NoPosition))(NoPosition), Some(FullPerm()(NoPosition)))(NoPosition)
     val testMethod : Method = Method("m1", Seq(), Seq(), Seq(), Seq(),
       Some(Seqn(Seq(
         Assume(assumeBody)(NoPosition)

From fe188404530dd080d26755228568dd64ca8cf17d Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 22 Oct 2024 15:11:01 +0200
Subject: [PATCH 10/12] Fixed assertion

---
 src/main/scala/viper/silver/parser/Translator.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 600cbf6fa..6637fd283 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -307,7 +307,7 @@ case class Translator(program: PProgram) {
         // A PrediateAccessPredicate is a PredicateResourceAccess combined with
         // a Permission. Havoc expects a ResourceAccess. To make types match,
         // we must extract the PredicateResourceAccess.
-        assert(perm.isInstanceOf[FullPerm])
+        assert(perm.isEmpty || perm.get.isInstanceOf[FullPerm])
         (newLhs, predAccess)
       case exp: MagicWand => (newLhs, exp)
       case _ => sys.error("Can't havoc this kind of expression")

From 999ef97a18f6d23c3d4a9e7114488b10d5df8540 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 22 Oct 2024 16:48:00 +0200
Subject: [PATCH 11/12] Renamed command line arg, allowing wildcard inside
 compound expressions in functions

---
 .../scala/viper/silver/ast/Expression.scala   |  4 +-
 src/main/scala/viper/silver/ast/Program.scala |  6 +-
 .../silver/ast/utility/Consistency.scala      | 63 +++++++++++++------
 .../silver/frontend/SilFrontEndConfig.scala   |  2 +-
 .../viper/silver/frontend/SilFrontend.scala   |  3 +
 5 files changed, 55 insertions(+), 23 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 7df446050..68d179f4c 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -288,7 +288,7 @@ object AccessPredicate {
 case class FieldAccessPredicate(loc: FieldAccess, permExp: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
   val perm = permExp.getOrElse(FullPerm()(pos, NoInfo, NoTrafos))
   override lazy val check : Seq[ConsistencyError] =
-    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq()) ++ Consistency.checkWildcardUsage(perm)
+    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq())
   val typ: Bool.type = Bool
 }
 
@@ -296,7 +296,7 @@ case class FieldAccessPredicate(loc: FieldAccess, permExp: Option[Exp])(val pos:
 case class PredicateAccessPredicate(loc: PredicateAccess, permExp: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AccessPredicate {
   val perm = permExp.getOrElse(FullPerm()(pos, NoInfo, NoTrafos))
   override lazy val check : Seq[ConsistencyError] =
-    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq()) ++ Consistency.checkWildcardUsage(perm)
+    (if(!(perm isSubtype Perm)) Seq(ConsistencyError(s"Permission amount parameter of access predicate must be of Perm type, but found ${perm.typ}", perm.pos)) else Seq())
   val typ: Bool.type = Bool
 }
 
diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index e8c3227ff..367edc4b9 100644
--- a/src/main/scala/viper/silver/ast/Program.scala
+++ b/src/main/scala/viper/silver/ast/Program.scala
@@ -361,7 +361,7 @@ case class Field(name: String, typ: Type)(val pos: Position = NoPosition, val in
 /** A predicate declaration. */
 case class Predicate(name: String, formalArgs: Seq[LocalVarDecl], body: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Location {
   override lazy val check : Seq[ConsistencyError] =
-    (if (body.isDefined) Consistency.checkNonPostContract(body.get) else Seq()) ++
+    (if (body.isDefined) Consistency.checkNonPostContract(body.get) ++ Consistency.checkWildcardUsage(body.get, false) else Seq()) ++
     (if (body.isDefined && !Consistency.noOld(body.get))
       Seq(ConsistencyError("Predicates must not contain old expressions.",body.get.pos))
      else Seq()) ++
@@ -426,7 +426,8 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
     body.fold(Seq.empty[ConsistencyError])(Consistency.checkNoArgsReassigned(formalArgs, _)) ++
     (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
+    checkReturnsNotUsedInPreconditions ++
+    (pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, false)) ++
 
   lazy val checkReturnsNotUsedInPreconditions: Seq[ConsistencyError] = {
     val varsInPreconditions: Seq[LocalVar] = pres flatMap {_.deepCollect {case l: LocalVar => l}}
@@ -454,6 +455,7 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres
     posts.flatMap(p=>{ if(!Consistency.noOld(p))
       Seq(ConsistencyError("Function post-conditions must not have old expressions.", p.pos)) else Seq()}) ++
     (pres ++ posts).flatMap(Consistency.checkNoPermForpermExceptInhaleExhale) ++
+    (pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, true)) ++
     (if(!(body forall (_ isSubtype typ))) Seq(ConsistencyError("Type of function body must match function type.", pos)) else Seq() ) ++
     (posts flatMap (p => if (!Consistency.noPerm(p) || !Consistency.noForPerm(p)) Seq(ConsistencyError("perm and forperm expressions are not allowed in function postconditions", p.pos)) else Seq() )) ++
     pres.flatMap(Consistency.checkPre) ++
diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala
index da06ed6f8..7e18f152c 100644
--- a/src/main/scala/viper/silver/ast/utility/Consistency.scala
+++ b/src/main/scala/viper/silver/ast/utility/Consistency.scala
@@ -15,6 +15,10 @@ import viper.silver.{FastMessage, FastMessaging}
 /** An utility object for consistency checking. */
 object Consistency {
   var messages: FastMessaging.Messages = Nil
+
+  // Set to enable legacy mode where permission amounts in function preconditions have their usual meaning instead
+  // of just just being treated as a kind of wildcard.
+  private var respectFunctionPrePermAmounts: Boolean = false
   def recordIfNot(suspect: Positioned, property: Boolean, message: String): Unit = {
     if (!property) {
       val pos = suspect.pos
@@ -23,6 +27,14 @@ object Consistency {
     }
   }
 
+  /** Use this method to enable consistency checks suitable for the legacy mode where permission amounts in function
+    * preconditions have their standard meaning, instead of always meaning a kind of wildcard.
+    * In other words, this should be set iff the command line flag "--respectFunctionPrePermAmounts" is set.
+    * */
+  def setFunctionPreconditionLegacyMode(enableLegacyMode: Boolean) = {
+    respectFunctionPrePermAmounts = enableLegacyMode
+  }
+
   def resetMessages(): Unit = { this.messages = Nil }
   @inline
   def recordIf(suspect: Positioned, property: Boolean, message: String): Unit =
@@ -185,19 +197,24 @@ object Consistency {
   }
 
   def warnAboutFunctionPermissionAmounts(f: Function): Seq[ConsistencyError] = {
+    if (respectFunctionPrePermAmounts)
+      return Seq()
     def hasSpecificPermAmounts(e: Exp): Boolean = e match {
       case CondExp(_, thn, els) => hasSpecificPermAmounts(thn) || hasSpecificPermAmounts(els)
       case _: FractionalPerm => true
+      case _: FullPerm => true
+      case _: PermAdd | _: PermSub | _: PermMinus | _: PermMul | _: IntPermMul | _: PermDiv | _: PermPermDiv => true
       case _ => false
     }
-    val preWarnings = f.pres.collect(pre => pre.collect{
-      case ap: AccessPredicate if hasSpecificPermAmounts(ap.perm) =>
-        ConsistencyError("Function precondition contains specific permission amount that will be treated like write/wildcard.", ap.pos, false)
-    }).flatten
-    val bodyWarnings = f.body.toSeq.map(body => body.collect{
-      case ap: AccessPredicate if hasSpecificPermAmounts(ap.perm) =>
-        ConsistencyError("Function body contains specific permission amount that will be treated like write/wildcard.", ap.pos, false)
-    }).flatten
+    def collectWarnings(e: Exp): Seq[ConsistencyError] = e.collect{
+      case FieldAccessPredicate(_, Some(perm)) if hasSpecificPermAmounts(perm) =>
+        ConsistencyError("Function contains specific permission amount that will be treated like wildcard.", perm.pos, false)
+      case PredicateAccessPredicate(_, Some(perm)) if hasSpecificPermAmounts(perm) =>
+        ConsistencyError("Function contains specific permission amount that will be treated like wildcard.", perm.pos, false)
+    }.toSeq
+
+    val preWarnings = f.pres.flatMap(collectWarnings)
+    val bodyWarnings = f.body.toSeq.flatMap(collectWarnings)
     preWarnings ++ bodyWarnings
   }
 
@@ -213,18 +230,28 @@ object Consistency {
     (if(!noLabelledOld(e)) Seq(ConsistencyError("Labelled-old expressions are not allowed in postconditions.", e.pos)) else Seq())
   }
 
-  def checkWildcardUsage(e: Exp): Seq[ConsistencyError] = {
-    val containedWildcards = e.shallowCollect{
-      case w: WildcardPerm => w
-    }
-    if (containedWildcards.nonEmpty) {
-      e match {
-        case _: WildcardPerm => Seq()
-        case _ => Seq(ConsistencyError("Wildcard occurs inside compound expression (should only occur directly in an accessibility predicate).", e.pos))
+  def checkWildcardUsage(n: Node, inFunction: Boolean): Seq[ConsistencyError] = {
+    if (!respectFunctionPrePermAmounts && inFunction)
+      return Seq()
+
+    def checkValidUse(e: Exp): Seq[ConsistencyError] = {
+      val containedWildcards = e.shallowCollect {
+        case w: WildcardPerm => w
+      }
+      if (containedWildcards.nonEmpty) {
+        e match {
+          case _: WildcardPerm => Seq()
+          case _ => Seq(ConsistencyError("Wildcard occurs inside compound expression (should only occur directly in an accessibility predicate).", e.pos))
+        }
+      } else {
+        Seq()
       }
-    } else {
-      Seq()
     }
+
+    n.collect{
+      case FieldAccessPredicate(_, Some(prm)) => checkValidUse(prm)
+      case PredicateAccessPredicate(_, Some(prm)) => checkValidUse(prm)
+    }.flatten.toSeq
   }
 
   /** checks that all quantified variables appear in all triggers */
diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
index 1ddcf82df..3462335e6 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
@@ -139,7 +139,7 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = false
   )
 
-  val respectFunctionPrecPermAmounts = opt[Boolean]("respectFunctionPrecPermAmounts",
+  val respectFunctionPrePermAmounts = opt[Boolean]("respectFunctionPrePermAmounts",
     descr = "Respects precise permission amounts in function preconditions instead of only checking read access.",
     default = Some(false),
     noshort = true,
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index ef779af25..486b27282 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -374,6 +374,9 @@ trait SilFrontend extends DefaultFrontend {
   }
 
   def doConsistencyCheck(input: Program): Result[Program] = {
+    if (config != null) {
+      Consistency.setFunctionPreconditionLegacyMode(config.respectFunctionPrePermAmounts())
+    }
     var errors = input.checkTransitively
     if (backendTypeFormat.isDefined)
       errors = errors ++ Consistency.checkBackendTypes(input, backendTypeFormat.get)

From aac52daab393e3ce98148e30ed54808aedd3af54 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 22 Oct 2024 17:05:59 +0200
Subject: [PATCH 12/12] Expanded test

---
 src/main/scala/viper/silver/ast/Program.scala |  2 +-
 .../functions/function_precondition_perms.vpr | 51 +++++++++++++++++++
 2 files changed, 52 insertions(+), 1 deletion(-)

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)