Skip to content

Commit

Permalink
adapts to avoid accidental printing of ASTs
Browse files Browse the repository at this point in the history
  • Loading branch information
ArquintL committed Jul 18, 2023
1 parent 4a27390 commit 04a7a2a
Showing 1 changed file with 7 additions and 14 deletions.
21 changes: 7 additions & 14 deletions src/main/scala/viper/gobra/reporting/Message.scala
Original file line number Diff line number Diff line change
Expand Up @@ -92,16 +92,14 @@ case class PreprocessedInputMessage(input: String, preprocessedContent: () => St
override val name: String = s"preprocessed_input_message"

override def toString: String = s"preprocessed_input_message(" +
s"file=$input, " +
s"content=${preprocessedContent()})"
s"file=$input)"
}

case class ParsedInputMessage(input: String, ast: () => PProgram) extends GobraMessage {
override val name: String = s"parsed_input_message"

override def toString: String = s"parsed_input_message(" +
s"file=$input, " +
s"ast=${ast().formatted})"
s"file=$input)"
}

case class ParserErrorMessage(input: Path, result: Vector[ParserError]) extends GobraMessage {
Expand Down Expand Up @@ -142,33 +140,29 @@ case class TypeCheckDebugMessage(inputs: Vector[String], ast: () => PPackage, de
override val name: String = s"type_check_debug_message"

override def toString: String = s"type_check_debug_message(" +
s"files=$inputs, " +
s"debugInfo=${debugTypeInfo()})"
s"files=$inputs)"
}

case class DesugaredMessage(inputs: Vector[String], internal: () => in.Program) extends GobraMessage {
override val name: String = s"desugared_message"

override def toString: String = s"desugared_message(" +
s"files=$inputs, " +
s"internal=${internal().formatted})"
s"files=$inputs)"
}

case class AppliedInternalTransformsMessage(inputs: Vector[String], internal: () => in.Program) extends GobraMessage {
override val name: String = s"transform_message"

override def toString: String = s"transform_message(" +
s"files=$inputs, " +
s"internal=${internal().formatted})"
s"files=$inputs)"
}

case class GeneratedViperMessage(taskName: String, inputs: Vector[String], vprAst: () => vpr.Program, backtrack: () => BackTranslator.BackTrackInfo) extends GobraMessage {
override val name: String = s"generated_viper_message"

override def toString: String = s"generated_viper_message(" +
s"taskName=$taskName" +
s"files=$inputs, " +
s"vprFormated=$vprAstFormatted)"
s"files=$inputs)"

lazy val vprAstFormatted: String = silver.ast.pretty.FastPrettyPrinter.pretty(vprAst())
}
Expand All @@ -185,8 +179,7 @@ case class ChoppedViperMessage(inputs: Vector[String], idx: Int, vprAst: () => v
override val name: String = s"chopped_viper_message"

override def toString: String = s"chopped_viper_message(" +
s"file=$inputs, " +
s"vprFormated=$vprAstFormatted)"
s"file=$inputs)"

lazy val vprAstFormatted: String = silver.ast.pretty.FastPrettyPrinter.pretty(vprAst())
}
Expand Down

0 comments on commit 04a7a2a

Please sign in to comment.