Fix issue 491

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

@@ -518,7 +518,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case PermTExpr() => "perm"
     case PointerTExpr(elem) => "*" <> showExpr(elem)
     case StructTExpr(fs) => "struct" <> braces(showList(fs)(f => f._1 <> ":" <+> showExpr(f._2)))
-    case ArrayTExpr(len, elem) => brackets(showExpr(len)) <> showExpr(elem)
+    case ArrayTExpr(len, elem) => brackets(len.toString()) <> showExpr(elem)
     case SliceTExpr(elem) => brackets(emptyDoc) <> showExpr(elem)
     case MapTExpr(key, elem) => "map" <> brackets(showExpr(key) <> comma <+> showExpr(elem))
     case SequenceTExpr(elem) => "seq" <> brackets(showExpr(elem))
@@ -532,6 +532,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case DfltVal(typ) => "dflt" <> brackets(showType(typ))
     case Tuple(args) => parens(showExprList(args))
     case Deref(exp, _) => "*" <> showExpr(exp)
+    case UncheckedRef(ref, _) => "&" <> showAddressable(ref)
     case Ref(ref, _) => "&" <> showAddressable(ref)
     case FieldRef(recv, field) => showExpr(recv) <> "."  <> field.name
     case StructUpdate(base, field, newVal) => showExpr(base) <> brackets(showField(field) <+> ":=" <+> showExpr(newVal))

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

@@ -604,7 +604,7 @@ case class Float32TExpr()(val info: Source.Parser.Info) extends TypeExpr
 case class Float64TExpr()(val info: Source.Parser.Info) extends TypeExpr
 case class IntTExpr(kind: IntegerKind)(val info: Source.Parser.Info) extends TypeExpr
 case class StructTExpr(fields: Vector[(String, Expr, Boolean)])(val info: Source.Parser.Info) extends TypeExpr
-case class ArrayTExpr(length: Expr, elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
+case class ArrayTExpr(length: BigInt, elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
 case class SliceTExpr(elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
 case class MapTExpr(keys: Expr, elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
 case class PermTExpr()(val info: Source.Parser.Info) extends TypeExpr
@@ -947,7 +947,18 @@ case class Deref(exp: Expr, underlyingTypeExpr: Type)(val info: Source.Parser.In
   override val typ: Type = underlyingTypeExpr.asInstanceOf[PointerT].t
 }
 
-case class Ref(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr with Location
+/** Only used internally to separate the type encodings. Should not be created by the desugarer. */
+case class UncheckedRef(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr {
+  def checked: Ref = Ref(ref, typ)(info)
+}
+
+object UncheckedRef {
+  def apply(exp: Expr)(info: Source.Parser.Info): UncheckedRef = Ref(exp)(info).unchecked
+}
+
+case class Ref(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr {
+  def unchecked: UncheckedRef = UncheckedRef(ref, typ)(info)
+}
 
 object Ref {
   def apply(ref: Expr)(info: Source.Parser.Info): Ref = {

src/main/scala/viper/gobra/ast/internal/theory/Comparability.scala

@@ -42,7 +42,7 @@ object Comparability {
 
     case _: TypeHead.StructHD => Kind.Recursive
     case _: TypeHead.FunctionHD => Kind.NonComparable
-    case TypeHead.ArrayHD => Kind.Recursive
+    case _: TypeHead.ArrayHD => Kind.Recursive
     case TypeHead.SliceHD => Kind.NonComparable
     case TypeHead.MapHD => Kind.NonComparable
     case _: TypeHead.InterfaceHD => Kind.Dynamic

src/main/scala/viper/gobra/ast/internal/theory/TypeHead.scala

@@ -27,7 +27,7 @@ object TypeHead {
   case class FunctionHD(arity: Int) extends TypeHead
   /** 'fields' stores for each field the name and whether the field is ghost. */
   case class StructHD(fields: Vector[(String, Boolean)]) extends TypeHead
-  case object ArrayHD extends TypeHead
+  case class ArrayHD(size: BigInt) extends TypeHead
   case object SliceHD extends TypeHead
   case object MapHD extends TypeHead
   case class InterfaceHD(name: String) extends TypeHead
@@ -72,7 +72,7 @@ object TypeHead {
     case VoidT => UnitHD
     case _: PermissionT => PermHD
     case SortT => SortHD
-    case _: ArrayT => ArrayHD
+    case t: ArrayT => ArrayHD(t.length)
     case _: SliceT => SliceHD
     case _: MapT => MapHD
     case _: SequenceT => SeqHD
@@ -145,7 +145,7 @@ object TypeHead {
     case _: PointerTExpr => PointerHD
     case t: DefinedTExpr => DefinedHD(t.name)
     case t: StructTExpr => StructHD(t.fields.map(t => (t._1, t._3)))
-    case _: ArrayTExpr => ArrayHD
+    case t: ArrayTExpr => ArrayHD(t.length)
     case _: SliceTExpr => SliceHD
     case _: MapTExpr => MapHD
     case _: PermTExpr => PermHD
@@ -168,7 +168,7 @@ object TypeHead {
     case _: DefinedHD => 0
     case t: FunctionHD => t.arity
     case t: StructHD => t.fields.size
-    case ArrayHD => 1
+    case _: ArrayHD => 1
     case SliceHD => 1
     case MapHD => 2
     case _: InterfaceHD => 0
@@ -187,5 +187,13 @@ object TypeHead {
     case t: PredHD => t.arity
   }
 
-
+  def isZeroSize(t: Type)(ctx: LookupTable): Boolean = isZeroSize(typeTree(t))(ctx)
+  def isZeroSize(t: RoseTree[TypeHead])(ctx: LookupTable): Boolean = {
+    t match {
+      case RoseTree(_: StructHD, children) => children.forall(isZeroSize(_)(ctx))
+      case RoseTree(hd: ArrayHD, children) => hd.size == 0 || children.forall(isZeroSize(_)(ctx))
+      case RoseTree(hd: DefinedHD, _) => isZeroSize(ctx.lookup(DefinedT(hd.name, Addressability.Exclusive)))(ctx)
+      case _ => false
+    }
+  }
 }

src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala

@@ -229,7 +229,7 @@ object CGEdgesTerminationTransform extends InternalTransform {
       case in.IntT(_, kind) => in.IntTExpr(kind)(src)
       case in.StringT(_) => in.StringTExpr()(src)
       case in.PermissionT(_) => in.PermTExpr()(src)
-      case in.ArrayT(length, elems, _) => in.ArrayTExpr(in.IntLit(length)(src), typeAsExpr(elems)(src))(src)
+      case in.ArrayT(length, elems, _) => in.ArrayTExpr(length, typeAsExpr(elems)(src))(src)
       case in.SliceT(elems, _) => in.SliceTExpr(typeAsExpr(elems)(src))(src)
       case in.MapT(keys, values, _) => in.MapTExpr(typeAsExpr(keys)(src), typeAsExpr(values)(src))(src)
       case in.SequenceT(t, _) => in.SequenceTExpr(typeAsExpr(t)(src))(src)

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

@@ -1298,7 +1298,7 @@ object Desugar {
             *
             * var i int = 0
             * var i0 int = 0 // since 'i' can change in the iteration we store the true index in i0
-            * var j elem(x) // [v] the type of the elements of x 
+            * var j elem(x) // [v] the type of the elements of x
             *
             * c := x // save the value of the slice/array since changing it doesn't change the iteration
             *
@@ -1490,7 +1490,7 @@ object Desugar {
             * if (len(c) > 0) {
             *     expIndex = 0
             * }
-            * 
+            *
             * if (0 <= expIndex && expIndex < len(c)) { // [v]
             *     expValue = c[expIndex]
             * }
@@ -1579,7 +1579,7 @@ object Desugar {
                 val valueSrc = meta(ass(1), info)
                 val valueAss = singleAss(valueLeft, in.IndexedExp(copiedVar, indexLeft.op, typ)(valueSrc))(valueSrc)
                 val updateValue = in.If(in.And(cond, in.AtLeastCmp(indexLeft.op, in.IntLit(0)(valueSrc))(valueSrc))(valueSrc), valueAss, in.Seqn(Vector())(valueSrc))(valueSrc)
-                
+
                 val indexValueEq = in.Implication(
                   in.LessCmp(in.IntLit(0)(indexSrc), length)(indexSrc),
                   in.Implication(
@@ -2584,9 +2584,8 @@ object Desugar {
 
         case PArrayType(len, elem) =>
           for {
-            inLen <- exprD(ctx, info)(len)
             inElem <- go(elem)
-          } yield in.ArrayTExpr(inLen, inElem)(src)
+          } yield in.ArrayTExpr(info.evalInt(len), inElem)(src)
 
         case PSliceType(elem) =>
           for {

src/main/scala/viper/gobra/frontend/info/TypeInfo.scala

@@ -43,4 +43,9 @@ trait TypeInfo extends ExternalTypeInfo {
   def freeDeclared(n: PNode): Vector[PIdnNode]
 
   def capturedVariables(decl: PClosureDecl): Vector[PIdnNode]
+
+  def evalBool(exp: PExpression): Boolean
+  def evalInt(exp: PExpression): BigInt
+  def evalString(exp: PExpression): String
+  def evalPerm(exp: PExpression): (BigInt, BigInt)
 }

src/main/scala/viper/gobra/frontend/info/implementation/property/ConstantEvaluation.scala

@@ -15,6 +15,23 @@ import viper.gobra.util.Violation.violation
 
 trait ConstantEvaluation { this: TypeInfoImpl =>
 
+  def evalBool(exp: PExpression): Boolean = {
+    boolConstantEval(exp).getOrElse(violation(s"expected constant bool expression, but got $exp"))
+  }
+
+  def evalInt(exp: PExpression): BigInt = {
+    intConstantEval(exp).getOrElse(violation(s"expected constant int expression, but got $exp"))
+  }
+
+  def evalString(exp: PExpression): String = {
+    stringConstantEval(exp).getOrElse(violation(s"expected constant string expression, but got $exp"))
+  }
+
+  def evalPerm(exp: PExpression): (BigInt, BigInt) = {
+    permConstantEval(exp).getOrElse(violation(s"expected constant permission expression, but got $exp"))
+  }
+
+
   lazy val boolConstantEval: PExpression => Option[Boolean] =
     attr[PExpression, Option[Boolean]] {
       case PBoolLit(lit) => Some(lit)

src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala

@@ -85,7 +85,7 @@ object DefaultErrorBackTranslator {
 
     val transformVerificationErrorReason: VerificationErrorReason => VerificationErrorReason = {
       case AssertionFalseError(info / OverflowCheckAnnotation) => OverflowErrorReason(info)
-      case AssertionFalseError(info / ReceiverNotNilCheckAnnotation) => InterfaceReceiverIsNilReason(info)
+      case AssertionFalseError(info / ReceiverNotNilCheckAnnotation) => ReceiverIsNilReason(info)
       case AssertionFalseError(info / RangeVariableMightNotExistAnnotation(_)) => AssertionFalseError(info)
       case x => x
     }

src/main/scala/viper/gobra/reporting/VerifierError.scala

@@ -157,6 +157,11 @@ case class CallError(info: Source.Verifier.Info) extends VerificationError {
   override def localMessage: String = "Call might fail"
 }
 
+case class DerefError(info: Source.Verifier.Info) extends VerificationError {
+  override def localId: String = "dereference_error"
+  override def localMessage: String = "Dereference might fail"
+}
+
 case class PostconditionError(info: Source.Verifier.Info) extends VerificationError {
   override def localId: String = "postcondition_error"
   override def localMessage: String = "Postcondition might not hold"
@@ -415,9 +420,9 @@ case class OverflowErrorReason(node: Source.Verifier.Info) extends VerificationE
   override def message: String = s"Expression ${node.origin.tag.trim} might cause integer overflow."
 }
 
-case class InterfaceReceiverIsNilReason(node: Source.Verifier.Info) extends VerificationErrorReason {
+case class ReceiverIsNilReason(node: Source.Verifier.Info) extends VerificationErrorReason {
   override def id: String = "receiver_is_nil_error"
-  override def message: String = s"The receiver might be nil"
+  override def message: String = s"The receiver ${node.origin.tag.trim} might be nil"
 }
 
 case class DynamicValueNotASubtypeReason(node: Source.Verifier.Info) extends VerificationErrorReason {

src/main/scala/viper/gobra/translator/context/Context.scala

@@ -95,6 +95,8 @@ trait Context {
 
   def reference(x: in.Location): CodeWriter[vpr.Exp] = typeEncoding.reference(this)(x)
 
+  def safeReference(x: in.Location): CodeWriter[vpr.Exp] = typeEncoding.safeReference(this)(x)
+
   def footprint(x: in.Location, perm: in.Expr): CodeWriter[vpr.Exp] = typeEncoding.addressFootprint(this)(x, perm)
 
   def isComparable(x: in.Expr): Either[Boolean, CodeWriter[vpr.Exp]] = typeEncoding.isComparable(this)(x)
@@ -132,15 +134,14 @@ trait Context {
   }
 
   // mapping
-
   def addVars(vars: vpr.LocalVarDecl*): Context
 
   // fresh variable counter
   /** publicly exposed infinite iterator providing fresh names */
   def freshNames: Iterator[String] = internalFreshNames
 
   /** internal fresh name iterator that additionally provides a getter function for its counter value */
-  protected def internalFreshNames: FreshNameIterator
+  protected def internalFreshNames: Context.FreshNameIterator
 
   /** copy constructor */
   def :=(
@@ -159,7 +160,28 @@ trait Context {
           unknownValueN: UnknownValues = unknownValue,
           typeEncodingN: TypeEncoding = typeEncoding,
           defaultEncodingN: DefaultEncoding = defaultEncoding,
-          initialFreshCounterValueN: Int = internalFreshNames.getValue
+          initialFreshCounterValueN: Option[Int] = None,
+        ): Context = {
+    update(fieldN, arrayN, seqToSetN, seqToMultisetN, seqMultiplicityN, optionN, optionToSeqN, sliceN, fixpointN, tupleN, equalityN, conditionN, unknownValueN, typeEncodingN, defaultEncodingN, initialFreshCounterValueN)
+  }
+
+  protected def update(
+          fieldN: Fields,
+          arrayN: Arrays,
+          seqToSetN: SeqToSet,
+          seqToMultisetN: SeqToMultiset,
+          seqMultiplicityN: SeqMultiplicity,
+          optionN: Options,
+          optionToSeqN: OptionToSeq,
+          sliceN: Slices,
+          fixpointN: Fixpoint,
+          tupleN: Tuples,
+          equalityN: Equality,
+          conditionN: Conditions,
+          unknownValueN: UnknownValues,
+          typeEncodingN: TypeEncoding,
+          defaultEncodingN: DefaultEncoding,
+          initialFreshCounterValueN: Option[Int],
         ): Context
 
 
@@ -183,8 +205,10 @@ trait Context {
     col.finalize(typeEncoding)
   }
 
+}
+
+object Context {
   trait FreshNameIterator extends Iterator[String] {
     def getValue: Int
   }
-
-}
+}