Skip to content

Commit

Permalink
more none.get
Browse files Browse the repository at this point in the history
  • Loading branch information
Naum-Tomov committed Oct 12, 2023
1 parent bc35ffd commit 5e383b5
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 4 deletions.
4 changes: 2 additions & 2 deletions src/rewrite/vct/rewrite/InlineApplicables.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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()}")
)
Expand Down
2 changes: 1 addition & 1 deletion src/rewrite/vct/rewrite/lang/LangJavaToCol.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand Down
2 changes: 1 addition & 1 deletion src/viper/viper/api/transform/SilverToCol.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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)),
Expand Down

0 comments on commit 5e383b5

Please sign in to comment.