Fixes #620

src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala

@@ -478,7 +478,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case PureLet(left, right, exp) =>
       "let" <+> showVar(left) <+> "==" <+> parens(showExpr(right)) <+> "in" <+> showExpr(exp)
 
-    case Old(op, _) => "old" <> parens(showExpr(op))
+    case Old(op) => "old" <> parens(showExpr(op))
 
     case LabeledOld(label, operand) => "old" <> brackets(showProxy(label)) <> parens(showExpr(operand))
 

src/main/scala/viper/gobra/ast/internal/Program.scala

@@ -563,10 +563,12 @@ case class PureLet(left: LocalVar, right: Expr, in: Expr)(val info: Source.Parse
 
 case class Let(left: LocalVar, right: Expr, in: Assertion)(val info: Source.Parser.Info) extends Assertion
 
-case class Old(operand: Expr, typ: Type)(val info: Source.Parser.Info) extends Expr
+case class Old(operand: Expr)(val info: Source.Parser.Info) extends Expr {
+  override def typ: Type = operand.typ.withAddressability(Addressability.rValue)
+}
 
 case class LabeledOld(label: LabelProxy, operand: Expr)(val info: Source.Parser.Info) extends Expr {
-  override val typ: Type = operand.typ
+  override val typ: Type = operand.typ.withAddressability(Addressability.rValue)
 }
 
 case class Conditional(cond: Expr, thn: Expr, els: Expr, typ: Type)(val info: Source.Parser.Info) extends Expr

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -4291,7 +4291,7 @@ object Desugar extends LazyLogging {
       val typ = typeD(info.typ(expr), info.addressability(expr))(src)
 
       expr match {
-        case POld(op) => for {o <- go(op)} yield in.Old(o, typ)(src)
+        case POld(op) => for {o <- go(op)} yield in.Old(o)(src)
         case PLabeledOld(l, op) => for {o <- go(op)} yield in.LabeledOld(labelProxy(l), o)(src)
         case PBefore(op) => for {o <- go(op)} yield in.LabeledOld(in.LabelProxy("before")(src), o)(src)
         case PConditional(cond, thn, els) =>  for {

src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala

@@ -21,7 +21,7 @@ class AssertionEncoding extends Encoding {
   import viper.gobra.translator.util.ViperWriter.CodeLevel._
 
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
-    case n@ in.Old(op, _) => for { o <- ctx.expression(op)} yield withSrc(vpr.Old(o), n)
+    case n@ in.Old(op) => for { o <- ctx.expression(op)} yield withSrc(vpr.Old(o), n)
     case n@ in.LabeledOld(l, op) => for {o <- ctx.expression(op)} yield withSrc(vpr.LabelledOld(o, l.name), n)
 
     case n@ in.Negation(op) => for{o <- ctx.expression(op)} yield withSrc(vpr.Not(o), n)

src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala

@@ -483,7 +483,7 @@ class BuiltInEncoding extends Encoding {
             i => in.ExprAssertion(
               in.GhostEqCmp(
                 in.IndexedExp(resultParam, i, sliceType)(src),
-                in.Old(in.IndexedExp(sliceParam, i, sliceType)(src), elemType)(src)
+                in.Old(in.IndexedExp(sliceParam, i, sliceType)(src))(src)
               )(src)
             )(src)
           }
@@ -586,7 +586,7 @@ class BuiltInEncoding extends Encoding {
             in.ExprAssertion(
               in.GhostEqCmp(
                 in.IndexedExp(dstParam, i, dstUnderlyingType)(src),
-                in.Old(in.IndexedExp(srcParam, i, srcUnderlyingType)(src), srcUnderlyingType.elems)(src)
+                in.Old(in.IndexedExp(srcParam, i, srcUnderlyingType)(src))(src)
               )(src)
             )(src)
           }
@@ -598,7 +598,7 @@ class BuiltInEncoding extends Encoding {
             in.ExprAssertion(
               in.GhostEqCmp(
                 in.IndexedExp(dstParam, i, dstUnderlyingType)(src),
-                in.Old(in.IndexedExp(dstParam, i, dstUnderlyingType)(src), dstUnderlyingType.elems)(src)
+                in.Old(in.IndexedExp(dstParam, i, dstUnderlyingType)(src))(src)
               )(src)
             )(src)
           }

src/test/resources/regressions/issues/000620-1.gobra

@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+type MyType struct {
+	x int
+}
+
+func main() {
+	mySlice := make([]MyType, 0)
+	snd := []MyType{MyType{1}}
+	mySlice = append(perm(1/2), mySlice, snd...)
+}

src/test/resources/regressions/issues/000620-2.gobra

@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+type MyStruct struct {
+    x int
+}
+
+func test() {
+    myStruct @ := MyStruct{42}
+    l:
+    assert myStruct == old[l](myStruct)
+}

src/test/resources/regressions/issues/000620-3.gobra

@@ -0,0 +1,10 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+func test() {
+    myInt @ := 42
+    l:
+    assert myInt == old[l](myInt)
+}