Fix inhale exhale exp

viperproject · Mar 1, 2025 · 8a32a03 · 8a32a03
1 parent 2ad28a0
commit 8a32a03
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 3 deletions.
diff --git a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
@@ -492,7 +492,7 @@ object PSymOp {
   type Dot = PReserved[Dot.type]
   case object DotDot  extends PSym("..")  with PSymbolOp
   type DotDot = PReserved[DotDot.type]
-  case object Comma   extends PSym(",")   with PSymbolOp
+  case object Comma   extends PSym(",")   with PSymbolOp with RightSpace
   type Comma = PReserved[Comma.type]
   case object RParen  extends PSym(")")   with PSymbolOp
   type RParen = PReserved[RParen.type]

diff --git a/src/test/resources/reformatter/methods.vpr b/src/test/resources/reformatter/methods.vpr
@@ -127,4 +127,7 @@ method empty_assign() {
    */
 
     swap(a, pivotIndex, right)
-}
+}
+
+method with_inhale_exhale(lock: Ref)
+    ensures [true,forperm r: Ref [r.held] :: false]
diff --git a/src/test/resources/reformatter/methods_expected.vpr b/src/test/resources/reformatter/methods_expected.vpr
@@ -131,4 +131,7 @@ method empty_assign() {
    */
 
     swap(a, pivotIndex, right)
-}
+}
+
+method with_inhale_exhale(lock: Ref)
+    ensures [true, forperm r: Ref [r.held] :: false]