fixed more None.get-s

src/col/vct/col/origin/Blame.scala

@@ -15,17 +15,17 @@ sealed trait ContractFailure {
 case class ContractFalse(node: Expr[_]) extends ContractFailure {
   override def code: String = "false"
   override def descCompletion: String = "this expression may be false"
-  override def inlineDescCompletion: String = s"`${node.o.getInlineContext.get.inlineContext}` may be false"
+  override def inlineDescCompletion: String = s"`${node.o.getInlineContextOrElse()}` may be false"
 }
 case class InsufficientPermissionToExhale(node: Expr[_]) extends ContractFailure {
   override def code: String = "perm"
   override def descCompletion: String = "there might not be enough permission to exhale this amount"
-  override def inlineDescCompletion: String = s"there might be insufficient permission for `${node.o.getInlineContext.get.inlineContext}`"
+  override def inlineDescCompletion: String = s"there might be insufficient permission for `${node.o.getInlineContextOrElse()}`"
 }
 case class NegativePermissionValue(node: Expr[_]) extends ContractFailure {
   override def code: String = "negativePermValue"
   override def descCompletion: String = "the amount of permission in this permission predicate may be negative"
-  override def inlineDescCompletion: String = s"`${node.o.getInlineContext.get.inlineContext}` may be a negative permission amount"
+  override def inlineDescCompletion: String = s"`${node.o.getInlineContextOrElse()}` may be a negative permission amount"
 }
 
 trait VerificationFailure {
@@ -76,9 +76,9 @@ trait NodeVerificationFailure extends VerificationFailure {
   def descInContext: String
   def inlineDescWithSource(source: String): String
 
-  override def position: String = node.o.getShortPosition.get.shortPosition
+  override def position: String = node.o.getShortPositionOrElse()
   override def desc: String = node.o.messageInContext(descInContext + errUrl)
-  override def inlineDesc: String = inlineDescWithSource(node.o.getInlineContext.get.inlineContext)
+  override def inlineDesc: String = inlineDescWithSource(node.o.getInlineContextOrElse())
 }
 
 trait WithContractFailure extends VerificationFailure {
@@ -89,7 +89,7 @@ trait WithContractFailure extends VerificationFailure {
   def descInContext: String
   def inlineDescWithSource(node: String, failure: String): String
 
-  override def position: String = node.o.getShortPosition.get.shortPosition
+  override def position: String = node.o.getShortPositionOrElse()
 
   override def code: String = s"$baseCode:${failure.code}"
 
@@ -100,7 +100,7 @@ trait WithContractFailure extends VerificationFailure {
     ))
 
   override def inlineDesc: String =
-    inlineDescWithSource(node.o.getInlineContext.get.inlineContext, failure.inlineDescCompletion)
+    inlineDescWithSource(node.o.getInlineContextOrElse(), failure.inlineDescCompletion)
 }
 
 sealed trait ExpectedErrorFailure extends VerificationFailure {
@@ -109,14 +109,14 @@ sealed trait ExpectedErrorFailure extends VerificationFailure {
 
 case class ExpectedErrorTrippedTwice(err: ExpectedError, left: VerificationFailure, right: VerificationFailure) extends ExpectedErrorFailure {
   override def code: String = "trippedTwice"
-  override def position: String = err.errorRegion.getShortPosition.get.shortPosition
+  override def position: String = err.errorRegion.getShortPositionOrElse()
   override def desc: String = err.errorRegion.messageInContext(s"The expected error with code `${err.errorCode}` occurred multiple times." + errUrl)
   override def inlineDesc: String = s"The expected error with code `${err.errorCode}` occurred multiple times."
 }
 
 case class ExpectedErrorNotTripped(err: ExpectedError) extends ExpectedErrorFailure {
   override def code: String = "notTripped"
-  override def position: String = err.errorRegion.getShortPosition.get.shortPosition
+  override def position: String = err.errorRegion.getShortPositionOrElse()
   override def desc: String = err.errorRegion.messageInContext(s"The expected error with code `${err.errorCode}` was not encountered." + errUrl)
   override def inlineDesc: String = s"The expected error with code `${err.errorCode}` was not encountered."
 }
@@ -217,14 +217,14 @@ case class PostconditionFailed(path: Seq[AccountedDirection], failure: ContractF
 }
 case class TerminationMeasureFailed(applicable: ContractApplicable[_], apply: Invocation[_], measure: DecreasesClause[_]) extends ContractedFailure with VerificationFailure {
   override def code: String = "decreasesFailed"
-  override def position: String = measure.o.getShortPosition.get.shortPosition
+  override def position: String = measure.o.getShortPositionOrElse()
   override def desc: String = Origin.messagesInContext(Seq(
     applicable.o -> "Applicable may not terminate, since ...",
     apply.o -> "... from this invocation ...",
     measure.o -> "... this measure may not be bounded, or may not decrease.",
   ))
   override def inlineDesc: String =
-    s"`${apply.o.getInlineContext.get.inlineContext}` may not terminate, since `${measure.o.getInlineContext.get.inlineContext}` is not decreased or not bounded"
+    s"`${apply.o.getInlineContextOrElse()}` may not terminate, since `${measure.o.getInlineContextOrElse()}` is not decreased or not bounded"
 }
 case class ContextEverywhereFailedInPost(failure: ContractFailure, node: ContractApplicable[_]) extends ContractedFailure with WithContractFailure {
   override def baseCode: String = "contextPostFailed"
@@ -254,19 +254,19 @@ case class LoopInvariantNotMaintained(failure: ContractFailure, node: LoopInvari
 }
 case class LoopTerminationMeasureFailed(node: DecreasesClause[_]) extends LoopInvariantFailure with NodeVerificationFailure {
   override def code: String = "loopDecreasesFailed"
-  override def position: String = node.o.getShortPosition.get.shortPosition
+  override def position: String = node.o.getShortPositionOrElse()
   override def descInContext: String = "Loop may not terminate, since this measure may not be bounded, or may not decrease."
-  override def inlineDescWithSource(source: String): String = s"Loop may not terminate, since `${node.o.getInlineContext.get.inlineContext}` may be unbounded or nondecreasing"
+  override def inlineDescWithSource(source: String): String = s"Loop may not terminate, since `${node.o.getInlineContextOrElse()}` may be unbounded or nondecreasing"
 }
 case class ReceiverNotInjective(quantifier: Starall[_], resource: Expr[_]) extends VerificationFailure with AnyStarError {
   override def code: String = "notInjective"
   override def desc: String = Origin.messagesInContext(Seq(
     quantifier.o -> "This quantifier causes the resources in its body to be quantified, ...",
     resource.o   -> "... but this resource may not be unique with regards to the quantified variables.",
   ))
-  override def inlineDesc: String = s"The location of the permission predicate in `${resource.o.getInlineContext.get.inlineContext}` may not be unique with regards to the quantified variables."
+  override def inlineDesc: String = s"The location of the permission predicate in `${resource.o.getInlineContextOrElse()}` may not be unique with regards to the quantified variables."
 
-  override def position: String = resource.o.getShortPosition.get.shortPosition
+  override def position: String = resource.o.getShortPositionOrElse()
 }
 case class DivByZero(node: DividingExpr[_]) extends NodeVerificationFailure {
   override def code: String = "divByZero"
@@ -356,7 +356,7 @@ case class KernelPostconditionFailed(failure: ContractFailure, node: CGpgpuKerne
 }
 case class KernelPredicateNotInjective(kernel: CGpgpuKernelSpecifier[_], predicate: Expr[_]) extends KernelFailure {
   override def code: String = "kernelNotInjective"
-  override def position: String = predicate.o.getShortPosition.get.shortPosition
+  override def position: String = predicate.o.getShortPositionOrElse()
 
   override def desc: String =
     Origin.messagesInContext(Seq(
@@ -365,7 +365,7 @@ case class KernelPredicateNotInjective(kernel: CGpgpuKernelSpecifier[_], predica
     ))
 
   override def inlineDesc: String =
-    s"`${predicate.o.getInlineContext.get.inlineContext}` does not have a unique location for every thread, and it could not be simplified away."
+    s"`${predicate.o.getInlineContextOrElse()}` does not have a unique location for every thread, and it could not be simplified away."
 }
 
 sealed trait KernelBarrierFailure extends VerificationFailure
@@ -420,15 +420,15 @@ case class ParBarrierInvariantBroken(failure: ContractFailure, node: ParBarrier[
 sealed trait ParBlockFailure extends VerificationFailure
 case class ParPredicateNotInjective(block: ParBlock[_], predicate: Expr[_]) extends ParBlockFailure {
   override def code: String = "parNotInjective"
-  override def position: String = predicate.o.getShortPosition.get.shortPosition
+  override def position: String = predicate.o.getShortPositionOrElse()
   override def desc: String =
     Origin.messagesInContext(Seq(
       (block.o, "This parallel block causes the formulas in its body to be quantified over all threads, ..."),
       (predicate.o, "... but this expression could not be simplified, and the Perm location is not injective in the thread variables." + errUrl),
     ))
 
   override def inlineDesc: String =
-    s"`${predicate.o.getInlineContext.get.inlineContext}` does not have a unique location for every thread, and it could not be simplified away."
+    s"`${predicate.o.getInlineContextOrElse()}` does not have a unique location for every thread, and it could not be simplified away."
 }
 
 sealed trait ParBlockContractFailure extends ParBlockFailure

src/col/vct/col/origin/ExpectedError.scala

@@ -13,7 +13,7 @@ class ExpectedError(val errorCode: String, val errorRegion: Origin, val blame: B
   def trip(failure: VerificationFailure): Unit =
     tripped match {
       case None =>
-        logger.debug(s"Swallowing error code $errorCode at ${errorRegion.getShortPosition.get.shortPosition}")
+        logger.debug(s"Swallowing error code $errorCode at ${errorRegion.getShortPositionOrElse()}")
         tripped = Some(failure)
       case Some(leftFailure) =>
         blame.blame(ExpectedErrorTrippedTwice(this, leftFailure, failure))

src/col/vct/col/origin/Origin.scala

@@ -142,6 +142,10 @@ case class Origin(originContents: Seq[OriginContent]) extends Blame[Verification
     }
   }
 
+  def getInlineContextOrElse(ctx: String = "[unkonwn inline context]"): String = {
+    getInlineContext.getOrElse(InlineContext(ctx)).inlineContext
+  }
+
   def getInlineBipContext: Option[InlineBipContext] = {
     originContents.flatMap {
       case InlineBipContext(any) => Seq(InlineBipContext(any))
@@ -172,6 +176,10 @@ case class Origin(originContents: Seq[OriginContent]) extends Blame[Verification
     }
   }
 
+  def getShortPositionOrElse(shortPos: String = "[unknown position]"): String = {
+    getShortPosition.getOrElse(ShortPosition(shortPos)).shortPosition
+  }
+
   def getStartEndLines: Option[StartEndLines] = {
     originContents.flatMap {
       case StartEndLines(any) => Seq(StartEndLines(any))

src/parsers/vct/parsers/transform/JavaToCol.scala

@@ -138,7 +138,7 @@ case class JavaToCol[G](override val baseOrigin: Origin,
 
   def convert(implicit pair: ElementValuePairContext): Option[(String, Expr[G])] = pair match {
     case ElementValuePair0(name, _, ElementValue0(expr)) =>
-      logger.warn(s"Annotation array initializer at ${OriginProvider(pair).getShortPosition.get.shortPosition} is discarded")
+      logger.warn(s"Annotation array initializer at ${OriginProvider(pair).getShortPositionOrElse()} is discarded")
       None
     case ElementValuePair0(name, _, ElementValue1(expr)) => Some((convert(name), convert(expr)))
     case x => ??(x)

src/rewrite/vct/rewrite/InlineApplicables.scala

@@ -64,16 +64,16 @@ case object InlineApplicables extends RewriterBuilder {
   private def InlinedOrigin(definition: Origin, usages: Seq[Apply[_]]): Origin = Origin(
     Seq(
       PreferredName(definition.getPreferredNameOrElse()),
-      ShortPosition(usages.head.o.getShortPosition.get.shortPosition),
+      ShortPosition(usages.head.o.getShortPositionOrElse()),
       Context(usages.map(_.o.getContext.get.context).mkString(
           start = " Inlined from:\n" + Origin.HR,
           sep = Origin.HR + " ...Then inlined from:\n" + Origin.HR,
           end = "",
         ) + Origin.HR +
           " In definition:\n" + Origin.HR +
           definition.getContext.get.context),
-      InlineContext(s"${definition.getInlineContext.get.inlineContext} [inlined from] " +
-        s"${usages.head.o.getInlineContext.get.inlineContext}")
+      InlineContext(s"${definition.getInlineContextOrElse()} [inlined from] " +
+        s"${usages.head.o.getInlineContextOrElse()}")
     )
   )
 

src/viper/viper/api/backend/silicon/Silicon.scala

@@ -186,7 +186,7 @@ case class Silicon(
         report.e match {
           case Right(e) =>
             val o = e.o
-            logger.info(s"${o.getShortPosition.get.shortPosition}: inst: ${report.instances} (gen: ${report.maxGeneration}, cost: ${report.maxCost})")
+            logger.info(s"${o.getShortPositionOrElse()}: inst: ${report.instances} (gen: ${report.maxGeneration}, cost: ${report.maxCost})")
           case Left(n) =>
             logger.info(s"$n: inst: ${report.instances} (gen: ${report.maxGeneration}, cost: ${report.maxCost})")
         }

src/viper/viper/api/backend/silicon/SiliconLogListener.scala

@@ -82,7 +82,7 @@ class SiliconMemberLogListener(log: SiliconLogListener, member: Member, pcs: Pat
       currentTaskStack = updateTaskStack(currentTaskStack, superTask.get, Nil, Nil)
   }
 
-  def where(node: Node): Option[String] = Util.getOrigin(node).map(_.getShortPosition.get.shortPosition)
+  def where(node: Node): Option[String] = Util.getOrigin(node).map(_.getShortPositionOrElse())
 
   def printRecords(records: mutable.Map[Int, DataRecord], excludedBy: Map[Int, Int]): Unit = {
     for(record <- records.values.toSeq.sortBy(_.id)) {