fix tests

viperproject · Sep 21, 2023 · 9ed226d · 9ed226d
1 parent a01eda6
commit 9ed226d
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala
@@ -86,6 +86,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
         case p => Violation.violation(s"Unexpected invoke resolve, got $p")
       }
       case _: PLength | _: PCapacity => AddrMod.callResult
+      case _: PLet => AddrMod.rValue
       case _: PSliceExp => AddrMod.sliceExpr
       case _: PTypeAssertion => AddrMod.typeAssertionResult
       case _: PReceive => AddrMod.receive

diff --git a/src/test/resources/regressions/features/let/let_simple.gobra b/src/test/resources/regressions/features/let/let_simple.gobra
@@ -32,6 +32,10 @@ func (a *A) g(x int) {
 	fold a.Mem()
 }
 
+pred Q(x int) {
+	true
+}
+
 requires acc(x)
 requires Q(y)
 func impureLets(x *int, y int) {