From d125182ee2ebe23193c3cea319214ef291563325 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Mon, 20 May 2024 10:05:47 +0200
Subject: [PATCH 1/7] Implement first draft of an inhaling expression.

---
 src/main/scala/viper/silver/ast/Expression.scala       |  6 ++++++
 .../scala/viper/silver/ast/pretty/PrettyPrinter.scala  |  4 +++-
 .../scala/viper/silver/ast/utility/Expressions.scala   |  1 +
 src/main/scala/viper/silver/ast/utility/Nodes.scala    |  1 +
 src/main/scala/viper/silver/parser/FastParser.scala    |  7 ++++++-
 src/main/scala/viper/silver/parser/ParseAst.scala      |  8 ++++++++
 .../scala/viper/silver/parser/ParseAstKeyword.scala    |  2 ++
 src/main/scala/viper/silver/parser/Resolver.scala      |  2 ++
 src/main/scala/viper/silver/parser/Translator.scala    |  2 ++
 src/test/resources/wands/inhaling/test1.vpr            | 10 ++++++++++
 10 files changed, 41 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/wands/inhaling/test1.vpr

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 090d05228..bf2c48aa4 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -495,6 +495,12 @@ case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition,
   lazy val typ = body.typ
 }
 
+case class Inhaling(exp: 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) ++
+    (if(!(exp isSubtype Bool)) Seq(ConsistencyError(s"Assertion to inhale must be of type Bool, but found ${exp.typ}", exp.pos)) else Seq())
+  lazy val typ: Type = 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 cb2896faa..543bf0929 100644
--- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
+++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
@@ -770,7 +770,9 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       case Unfolding(acc, exp) =>
         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)))
+        parens(text("applying") <+> parens(nest(defaultIndent, show(wand))) <+> "in" <> nest(defaultIndent, line <> show(exp)))
+      case Inhaling(exp, body) =>
+        parens(text("inhaling") <+> parens(nest(defaultIndent, show(exp))) <+> "in" <> nest(defaultIndent, line <> show(body)))
       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 ac2b84ff4..2cf6b9323 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 inh: Inhaling => isPure(inh.body)
     case QuantifiedExp(_, e0) => isPure(e0)
     case Let(_, _, body) => isPure(body)
     case e: ExtensionExp => e.extensionIsPure
diff --git a/src/main/scala/viper/silver/ast/utility/Nodes.scala b/src/main/scala/viper/silver/ast/utility/Nodes.scala
index 0dc99d7dd..1e295bf32 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 Inhaling(acc, body) => Seq(acc, 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..610ced119 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -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", "inhaling", "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 "inhaling" => inhaling.map(_(PReserved(PKwOp.Inhaling)(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 inhaling[$: P]: P[PKwOp.Inhaling => Pos => PExp] = P(exp.parens ~ PKwOp.In ~ exp).map {
+    case (exp, in, body) => PInhaling(_, exp.inner, in, body)
+  }
+
   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 539a80fa8..d87739351 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1064,6 +1064,14 @@ 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 PInhaling(inhaling: PKwOp.Inhaling, exp: PExp, in: PKwOp.In, body: PExp)(val pos: (Position, Position)) extends PHeapOpApp {
+  override val args = Seq(exp, body)
+  override val signatures: List[PTypeSubstitution] = List(
+    Map(POpApp.pArgS(0) -> Bool, POpApp.pResS -> POpApp.pArg(1)),
+    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..8ab7d79cf 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 Inhaling    extends PKwOp("inhaling")                 with PKeywordAtom with RightSpace
+  type Inhaling = PReserved[Inhaling.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/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index c3280c3a3..bd674f0a6 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -707,6 +707,8 @@ case class TypeChecker(names: NameAnalyser) {
               case PApplying(_, wand, _, _) =>
                 checkMagicWand(wand)
 
+              case PInhaling(_, _, _, _) =>
+
               // We checked that the `rcv` is valid above with `poa.args.foreach(checkInternal)`
               case PFieldAccess(_, _, idnref) =>
                 if (idnref.decls.isEmpty)
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index ecc2fc4ec..021463a5a 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -507,6 +507,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 PInhaling(_, e, _, body) =>
+        Inhaling(exp(e), exp(body))(pos, info)
       case pl@PLet(_, _, _, exp1, _, PLetNestedScope(body)) =>
         Let(liftLogicalDecl(pl.decl), exp(exp1.inner), exp(body))(pos, info)
       case _: PLetNestedScope =>
diff --git a/src/test/resources/wands/inhaling/test1.vpr b/src/test/resources/wands/inhaling/test1.vpr
new file mode 100644
index 000000000..c40ee9900
--- /dev/null
+++ b/src/test/resources/wands/inhaling/test1.vpr
@@ -0,0 +1,10 @@
+field f: Int
+
+method test1(x: Ref, y: Ref)
+    requires acc(x.f) && acc(y.f)
+{
+    y.f := 10
+    package acc(x.f) --* acc(y.f)
+    exhale acc(x.f)
+    assert inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f == 10
+}

From eb72cbaa1ca393762bc43b91f528e497f51caf9c Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Mon, 20 May 2024 10:31:10 +0200
Subject: [PATCH 2/7] Move tests.

---
 src/test/resources/{wands => }/inhaling/test1.vpr | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename src/test/resources/{wands => }/inhaling/test1.vpr (100%)

diff --git a/src/test/resources/wands/inhaling/test1.vpr b/src/test/resources/inhaling/test1.vpr
similarity index 100%
rename from src/test/resources/wands/inhaling/test1.vpr
rename to src/test/resources/inhaling/test1.vpr

From 0ca6793bf0b213b17cdff2d2c6c1d85e1a48e454 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Mon, 20 May 2024 14:31:19 +0200
Subject: [PATCH 3/7] Add more tests, execute inhaling body in its own scope,
 and write documentation for executionFlowController.

---
 src/test/resources/inhaling/test1.vpr |  7 +++++--
 src/test/resources/inhaling/test2.vpr | 14 ++++++++++++++
 src/test/resources/inhaling/test3.vpr | 15 +++++++++++++++
 src/test/resources/inhaling/test4.vpr | 18 ++++++++++++++++++
 src/test/resources/inhaling/test5.vpr | 12 ++++++++++++
 src/test/resources/inhaling/test6.vpr |  9 +++++++++
 6 files changed, 73 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/inhaling/test2.vpr
 create mode 100644 src/test/resources/inhaling/test3.vpr
 create mode 100644 src/test/resources/inhaling/test4.vpr
 create mode 100644 src/test/resources/inhaling/test5.vpr
 create mode 100644 src/test/resources/inhaling/test6.vpr

diff --git a/src/test/resources/inhaling/test1.vpr b/src/test/resources/inhaling/test1.vpr
index c40ee9900..4b5c56f06 100644
--- a/src/test/resources/inhaling/test1.vpr
+++ b/src/test/resources/inhaling/test1.vpr
@@ -3,8 +3,11 @@ field f: Int
 method test1(x: Ref, y: Ref)
     requires acc(x.f) && acc(y.f)
 {
-    y.f := 10
+    y.f := 42
+
     package acc(x.f) --* acc(y.f)
     exhale acc(x.f)
-    assert inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f == 10
+
+    assert inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f == 42
+    assert acc(x.f, none)
 }
diff --git a/src/test/resources/inhaling/test2.vpr b/src/test/resources/inhaling/test2.vpr
new file mode 100644
index 000000000..b3f0ac344
--- /dev/null
+++ b/src/test/resources/inhaling/test2.vpr
@@ -0,0 +1,14 @@
+field f: Int
+
+method test2(x: Ref, y: Ref)
+    requires acc(x.f) && acc(y.f)
+{
+    x.f := 10
+    y.f := 42
+
+    exhale acc(x.f)
+
+    assert inhaling (acc(x.f)) in y.f == 42
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (acc(x.f)) in x.f == 10
+}
\ No newline at end of file
diff --git a/src/test/resources/inhaling/test3.vpr b/src/test/resources/inhaling/test3.vpr
new file mode 100644
index 000000000..dfb1355a4
--- /dev/null
+++ b/src/test/resources/inhaling/test3.vpr
@@ -0,0 +1,15 @@
+field f: Int
+
+predicate foo(x: Ref) { acc(x.f) }
+
+method test3(x: Ref, y: Ref)
+    requires foo(x) && foo(y)
+    requires unfolding foo(x) in x.f == 10
+    requires unfolding foo(y) in y.f == 42
+{
+    exhale foo(x)
+
+    assert inhaling (foo(x)) in unfolding foo(y) in y.f == 42
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (foo(x)) in unfolding foo(x) in x.f == 10
+}
\ No newline at end of file
diff --git a/src/test/resources/inhaling/test4.vpr b/src/test/resources/inhaling/test4.vpr
new file mode 100644
index 000000000..6389b4d61
--- /dev/null
+++ b/src/test/resources/inhaling/test4.vpr
@@ -0,0 +1,18 @@
+field f: Int
+
+method test4(x: Ref, y: Ref)
+    requires acc(x.f) && acc(y.f)
+{
+    x.f := 42
+    y.f := 10
+
+    package acc(x.f) --* acc(y.f)
+    exhale acc(x.f)
+
+    var p: Int := inhaling (acc(x.f)) in x.f
+    var q: Int := inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f
+
+    assert q == 10
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert p == 42
+}
diff --git a/src/test/resources/inhaling/test5.vpr b/src/test/resources/inhaling/test5.vpr
new file mode 100644
index 000000000..9809a0992
--- /dev/null
+++ b/src/test/resources/inhaling/test5.vpr
@@ -0,0 +1,12 @@
+field f: Int
+
+method test5a(x: Ref, y: Ref)
+    requires true --* acc(x.f)
+    requires acc(x.f) --* acc(y.f)
+    requires inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f == 10
+{
+    apply true --* acc(x.f)
+    apply acc(x.f) --* acc(y.f)
+
+    assert y.f == 10
+}
diff --git a/src/test/resources/inhaling/test6.vpr b/src/test/resources/inhaling/test6.vpr
new file mode 100644
index 000000000..b1f5548e7
--- /dev/null
+++ b/src/test/resources/inhaling/test6.vpr
@@ -0,0 +1,9 @@
+field f: Int
+
+method test6(x: Ref)
+    requires acc(x.f)
+{
+    assert inhaling (acc(x.f)) in true
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
\ No newline at end of file

From 8ccaedef4b662001b4295e87b55dbd774a1f5f7a Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Mon, 20 May 2024 14:31:23 +0200
Subject: [PATCH 4/7] Add more tests, execute inhaling body in its own scope,
 and write documentation for executionFlowController.

---
 src/main/scala/viper/silver/ast/utility/Nodes.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/ast/utility/Nodes.scala b/src/main/scala/viper/silver/ast/utility/Nodes.scala
index 1e295bf32..aec9f43b4 100644
--- a/src/main/scala/viper/silver/ast/utility/Nodes.scala
+++ b/src/main/scala/viper/silver/ast/utility/Nodes.scala
@@ -83,7 +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 Inhaling(acc, body) => Seq(acc, body)
+          case Inhaling(exp, body) => Seq(exp, body)
           case Old(exp) => Seq(exp)
           case CondExp(cond, thn, els) => Seq(cond, thn, els)
           case Let(v, exp, body) => Seq(v, exp, body)

From 25e4cc5e379d79652cf8bacfe7a1953e86e580cb Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Tue, 28 May 2024 11:37:40 +0200
Subject: [PATCH 5/7] Update the test cases.

---
 src/test/resources/inhaling/README.md | 11 +++++++++++
 src/test/resources/inhaling/test2.vpr |  2 +-
 src/test/resources/inhaling/test3.vpr |  2 +-
 src/test/resources/inhaling/test5.vpr |  2 +-
 src/test/resources/inhaling/test6.vpr | 11 +++++++++--
 src/test/resources/inhaling/test7.vpr | 27 +++++++++++++++++++++++++++
 6 files changed, 50 insertions(+), 5 deletions(-)
 create mode 100644 src/test/resources/inhaling/README.md
 create mode 100644 src/test/resources/inhaling/test7.vpr

diff --git a/src/test/resources/inhaling/README.md b/src/test/resources/inhaling/README.md
new file mode 100644
index 000000000..3d4b502e8
--- /dev/null
+++ b/src/test/resources/inhaling/README.md
@@ -0,0 +1,11 @@
+# Test Cases for inhaling expressions
+
+| Filename                 | Description                                                            |
+|--------------------------|------------------------------------------------------------------------|
+| [test1.vpr](./test1.vpr) | Inhaling magic wand's LHS to inspect its snapshot.                     |
+| [test2.vpr](./test2.vpr) | Inhaling single fields and inspect its values.                         |
+| [test3.vpr](./test3.vpr) | Inhaling predicates and inspect its values.                            |
+| [test4.vpr](./test4.vpr) | Inhaling fields and return some values.                                |
+| [test5.vpr](./test5.vpr) | Inhaling in a method's precondition to define a magic wand's snapshot. |
+| [test6.vpr](./test6.vpr) | Invalid inhaling of a field that should not allow us to prove false.   |           
+| [test7.vpr](./test7.vpr) | Inhaling fields with some conditions.                                  |
diff --git a/src/test/resources/inhaling/test2.vpr b/src/test/resources/inhaling/test2.vpr
index b3f0ac344..c2d1fa776 100644
--- a/src/test/resources/inhaling/test2.vpr
+++ b/src/test/resources/inhaling/test2.vpr
@@ -11,4 +11,4 @@ method test2(x: Ref, y: Ref)
     assert inhaling (acc(x.f)) in y.f == 42
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert inhaling (acc(x.f)) in x.f == 10
-}
\ No newline at end of file
+}
diff --git a/src/test/resources/inhaling/test3.vpr b/src/test/resources/inhaling/test3.vpr
index dfb1355a4..a33ac62e0 100644
--- a/src/test/resources/inhaling/test3.vpr
+++ b/src/test/resources/inhaling/test3.vpr
@@ -12,4 +12,4 @@ method test3(x: Ref, y: Ref)
     assert inhaling (foo(x)) in unfolding foo(y) in y.f == 42
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert inhaling (foo(x)) in unfolding foo(x) in x.f == 10
-}
\ No newline at end of file
+}
diff --git a/src/test/resources/inhaling/test5.vpr b/src/test/resources/inhaling/test5.vpr
index 9809a0992..3cf942292 100644
--- a/src/test/resources/inhaling/test5.vpr
+++ b/src/test/resources/inhaling/test5.vpr
@@ -1,6 +1,6 @@
 field f: Int
 
-method test5a(x: Ref, y: Ref)
+method test5(x: Ref, y: Ref)
     requires true --* acc(x.f)
     requires acc(x.f) --* acc(y.f)
     requires inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f == 10
diff --git a/src/test/resources/inhaling/test6.vpr b/src/test/resources/inhaling/test6.vpr
index b1f5548e7..1e32a19de 100644
--- a/src/test/resources/inhaling/test6.vpr
+++ b/src/test/resources/inhaling/test6.vpr
@@ -1,9 +1,16 @@
 field f: Int
 
-method test6(x: Ref)
+method test6a(x: Ref)
     requires acc(x.f)
 {
     assert inhaling (acc(x.f)) in true
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert false
-}
\ No newline at end of file
+}
+
+method test6b(x: Ref)
+    requires acc(x.f)
+{
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (acc(x.f)) in false
+}
diff --git a/src/test/resources/inhaling/test7.vpr b/src/test/resources/inhaling/test7.vpr
new file mode 100644
index 000000000..b307c9398
--- /dev/null
+++ b/src/test/resources/inhaling/test7.vpr
@@ -0,0 +1,27 @@
+field f: Int
+
+method test7a(x: Ref, y: Ref, i: Int)
+    requires acc(x.f) && acc(y.f)
+    requires y.f == 42
+{
+    package acc(x.f) --* acc(y.f)
+
+    if (i < 0) {
+        exhale acc(x.f)
+        assert inhaling (i < 0 ? acc(x.f) : true) in applying (acc(x.f) --* acc(y.f)) in y.f == 42
+    } else {
+        assert inhaling (i < 0 ? acc(x.f) : true) in applying (acc(x.f) --* acc(y.f)) in y.f == 42
+    }
+}
+
+method test7b(x: Ref, y: Ref, i: Int)
+    requires acc(x.f) && acc(y.f)
+    requires y.f == 42
+{
+    package acc(x.f) --* acc(y.f)
+    if (i < 0) {
+        exhale acc(x.f)
+    }
+
+    assert inhaling (i < 0 ? acc(x.f) : true) in applying (acc(x.f) --* acc(y.f)) in y.f == 42
+}

From b564483e653528d4554e4e82bef9deae3032f4cd Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Thu, 30 May 2024 10:52:30 +0200
Subject: [PATCH 6/7] Fix joining of execution paths after inhaling.

---
 src/test/resources/inhaling/README.md |  6 ++++--
 src/test/resources/inhaling/test6.vpr |  2 --
 src/test/resources/inhaling/test8.vpr | 15 +++++++++++++++
 src/test/resources/inhaling/test9.vpr | 14 ++++++++++++++
 4 files changed, 33 insertions(+), 4 deletions(-)
 create mode 100644 src/test/resources/inhaling/test8.vpr
 create mode 100644 src/test/resources/inhaling/test9.vpr

diff --git a/src/test/resources/inhaling/README.md b/src/test/resources/inhaling/README.md
index 3d4b502e8..00eaf9f3a 100644
--- a/src/test/resources/inhaling/README.md
+++ b/src/test/resources/inhaling/README.md
@@ -7,5 +7,7 @@
 | [test3.vpr](./test3.vpr) | Inhaling predicates and inspect its values.                            |
 | [test4.vpr](./test4.vpr) | Inhaling fields and return some values.                                |
 | [test5.vpr](./test5.vpr) | Inhaling in a method's precondition to define a magic wand's snapshot. |
-| [test6.vpr](./test6.vpr) | Invalid inhaling of a field that should not allow us to prove false.   |           
-| [test7.vpr](./test7.vpr) | Inhaling fields with some conditions.                                  |
+| [test6.vpr](./test6.vpr) | Invalid inhaling leads to a inconsistent state.                        |           
+| [test7.vpr](./test7.vpr) | Inhaling fields with conditionals.                                     |
+| [test8.vpr](./test8.vpr) | Inhaling fields with value conditions.                                 |
+| [test9.vpr](./test9.vpr) | Inhaling does not leak any permissions.                                |
diff --git a/src/test/resources/inhaling/test6.vpr b/src/test/resources/inhaling/test6.vpr
index 1e32a19de..55dd5c292 100644
--- a/src/test/resources/inhaling/test6.vpr
+++ b/src/test/resources/inhaling/test6.vpr
@@ -4,13 +4,11 @@ method test6a(x: Ref)
     requires acc(x.f)
 {
     assert inhaling (acc(x.f)) in true
-    //:: ExpectedOutput(assert.failed:assertion.false)
     assert false
 }
 
 method test6b(x: Ref)
     requires acc(x.f)
 {
-    //:: ExpectedOutput(assert.failed:assertion.false)
     assert inhaling (acc(x.f)) in false
 }
diff --git a/src/test/resources/inhaling/test8.vpr b/src/test/resources/inhaling/test8.vpr
new file mode 100644
index 000000000..5a5f466aa
--- /dev/null
+++ b/src/test/resources/inhaling/test8.vpr
@@ -0,0 +1,15 @@
+field f: Int
+
+method test8a(x: Ref)
+    requires acc(x.f)
+{
+    assert inhaling (x.f == 1) in x.f == 1
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (x.f == 1) in x.f == 0
+}
+
+method test8b(x: Ref) {
+    assert inhaling (acc(x.f) && x.f == 1) in x.f == 1
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (acc(x.f) && x.f == 1) in x.f == 0
+}
diff --git a/src/test/resources/inhaling/test9.vpr b/src/test/resources/inhaling/test9.vpr
new file mode 100644
index 000000000..b9332bed3
--- /dev/null
+++ b/src/test/resources/inhaling/test9.vpr
@@ -0,0 +1,14 @@
+field f: Int
+
+method test9a(x: Ref) {
+    assert inhaling (acc(x.f) && x.f == 0) in x.f == 0
+    assert acc(x.f, none)
+}
+
+method test9b(x: Ref, p: Perm)
+    requires none <= p
+    requires acc(x.f, p)
+{
+    assert inhaling (acc(x.f, write - p) && x.f == 0) in x.f == 0
+    assert acc(x.f, p)
+}

From db0aee3a4aaa8286cfb52121d129b27e05a63364 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Thu, 30 May 2024 11:26:08 +0200
Subject: [PATCH 7/7] Add test with predicates.

---
 src/test/resources/inhaling/test6.vpr | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/test/resources/inhaling/test6.vpr b/src/test/resources/inhaling/test6.vpr
index 55dd5c292..c446b7eb9 100644
--- a/src/test/resources/inhaling/test6.vpr
+++ b/src/test/resources/inhaling/test6.vpr
@@ -1,5 +1,9 @@
 field f: Int
 
+predicate P(x: Ref) {
+    acc(x.f) && x.f == 1
+}
+
 method test6a(x: Ref)
     requires acc(x.f)
 {
@@ -12,3 +16,12 @@ method test6b(x: Ref)
 {
     assert inhaling (acc(x.f)) in false
 }
+
+method test6c(x: Ref)
+    requires acc(x.f) && x.f == 0
+{
+    assert inhaling (P(x)) in x.f == 0
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (P(x)) in false
+    assert inhaling (P(x)) in unfolding P(x) in false
+}