From 5e383b5cdd0c378f1ef22104b1c47d5f42903ca3 Mon Sep 17 00:00:00 2001
From: Naum-Tomov <naum.tomov@gmail.com>
Date: Thu, 12 Oct 2023 14:36:49 +0200
Subject: [PATCH] more none.get

---
 src/rewrite/vct/rewrite/InlineApplicables.scala  | 4 ++--
 src/rewrite/vct/rewrite/lang/LangJavaToCol.scala | 2 +-
 src/viper/viper/api/transform/SilverToCol.scala  | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/rewrite/vct/rewrite/InlineApplicables.scala b/src/rewrite/vct/rewrite/InlineApplicables.scala
index 1bc74e5327..8e54d00e30 100644
--- a/src/rewrite/vct/rewrite/InlineApplicables.scala
+++ b/src/rewrite/vct/rewrite/InlineApplicables.scala
@@ -65,13 +65,13 @@ case object InlineApplicables extends RewriterBuilder {
     Seq(
       PreferredName(definition.getPreferredNameOrElse()),
       ShortPosition(usages.head.o.getShortPositionOrElse()),
-      Context(usages.map(_.o.getContext.get.context).mkString(
+      Context(usages.map(_.o.getContext.getOrElse(Context("[unknown context]")).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),
+          definition.getContext.getOrElse(Context("[unknown context]")).context),
       InlineContext(s"${definition.getInlineContextOrElse()} [inlined from] " +
         s"${usages.head.o.getInlineContextOrElse()}")
     )
diff --git a/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala b/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala
index 55b9d14672..d4a8265250 100644
--- a/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala
@@ -190,7 +190,7 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends
 
     declsDefault.foreach {
       case cons: JavaConstructor[Pre] =>
-        logger.debug(s"Constructor for ${cons.o.getContext.get.context}")
+        logger.debug(s"Constructor for ${cons.o.getContext.getOrElse(Context("[unknown context]")).context}")
         implicit val o: Origin = cons.o
         val t = TClass(ref)
         val resVar = new Variable[Post](t)(ThisVar())
diff --git a/src/viper/viper/api/transform/SilverToCol.scala b/src/viper/viper/api/transform/SilverToCol.scala
index 7038180cc6..21dc918b81 100644
--- a/src/viper/viper/api/transform/SilverToCol.scala
+++ b/src/viper/viper/api/transform/SilverToCol.scala
@@ -29,7 +29,7 @@ case object SilverToCol {
           val (start, end) = (pos.start, pos.end.getOrElse(pos.start))
           UserInputOrigin(
             RWFile(pos.file.toFile), start.line - 1, end.line - 1, Some((start.column - 1, end.column - 1))
-          ).getContext.get.context
+          ).getContext.getOrElse(Context("[unknown context]")).context
         case other => s"[Unknown silver position kind: $other]"
       }),
       InlineContext(InputOrigin.compressInlineText(node.toString)),