diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala
index f38cd8aef..5195f3210 100644
--- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala
+++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala
@@ -14,8 +14,11 @@ import viper.gobra.ast.frontend._
 import viper.gobra.util.{Binary, Hexadecimal, Octal}
 import viper.gobra.frontend.GobraParser._
 import viper.gobra.frontend.Parser.PRewriter
+import viper.gobra.frontend.Source.TransformableSource
 import viper.gobra.frontend.TranslationHelpers._
+import viper.gobra.reporting.{ParserError, ParserMessage, ParserWarning}
 import viper.gobra.util.Violation.violation
+import viper.silver.ast.{HasLineColumn, LineColumnPosition, SourcePosition}
 
 import scala.StringContext.InvalidEscapeException
 import scala.annotation.unused
@@ -2505,11 +2508,11 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
 
   //region Error reporting and positioning
 
-  private def fail(cause : NamedPositionable, msg : String = "") = {
+  private def fail(cause: NamedPositionable, msg: String = ""): Nothing = {
     throw TranslationFailure(cause, msg)
   }
 
-  private def unexpected(ctx: ParserRuleContext) = {
+  private def unexpected(ctx: ParserRuleContext): Nothing = {
     violation(s"could not translate '${ctx.getText}', got unexpected production '${visitChildren(ctx)}'")
   }
 
@@ -2581,17 +2584,42 @@ trait Named {
 
 // Any object that can be assigned a start and end in a source is positionable
 trait Positionable {
-  val startPos : Position
-  val endPos : Position
-  val startFinish : (Position, Position) = (startPos, endPos)
+  val startPos: Position
+  val endPos: Position
+  val startFinish: (Position, Position) = (startPos, endPos)
+  def start: HasLineColumn = LineColumnPosition(startPos.line, startPos.column)
+  def end: HasLineColumn = LineColumnPosition(endPos.line, endPos.column)
 }
 
 // This trait is used for error messages, here we need both a position and a name.
 sealed trait NamedPositionable extends Named with Positionable
 
+sealed trait TranslationMessage {
+  def toMessage(source: Source): ParserMessage
+}
+
+abstract class TranslationException(message: String) extends Exception(message) with TranslationMessage {
+  def cause: NamedPositionable
+}
+
+case class TranslationFailure(cause: NamedPositionable, details: String = "") extends TranslationException(s"Translation of ${cause.name} ${cause.text} failed${if (details.nonEmpty) ": " + details else "."}") {
+  override def toMessage(source: Source): ParserError = {
+    val pos = Some(SourcePosition(source.toPath, cause.start, cause.end))
+    ParserError(s"$getMessage ${getStackTrace.toVector(1)}", pos)
+  }
+}
 
-class TranslationException(@unused cause: NamedPositionable, msg : String) extends Exception(msg)
+case class TranslationWarning(cause: NamedPositionable, details: String = "") extends TranslationMessage {
+  val message = s"Warning in ${cause.name} ${cause.text}${if (details.nonEmpty) ": " + details else "."}"
+  override def toMessage(source: Source): ParserWarning = {
+    val pos = Some(SourcePosition(source.toPath, cause.start, cause.end))
+    ParserWarning(s"$message", pos)
+  }
+}
 
-case class TranslationFailure(cause: NamedPositionable, msg : String = "") extends TranslationException(cause, s"Translation of ${cause.name} ${cause.text} failed${if (msg.nonEmpty) ": " + msg else "."}")
-case class TranslationWarning(cause: NamedPositionable, msg : String = "") extends TranslationException(cause, s"Warning in ${cause.name} ${cause.text}${if (msg.nonEmpty) ": " + msg else "."}")
-case class UnsupportedOperatorException(cause: NamedPositionable, typ : String, msg : String = "") extends TranslationException(cause, s"Unsupported $typ operation: ${cause.text}.")
+case class UnsupportedOperatorException(cause: NamedPositionable, typ: String, msg: String = "") extends TranslationException(s"Unsupported $typ operation: ${cause.text}.") {
+  override def toMessage(source: Source): ParserError = {
+    val pos = Some(SourcePosition(source.toPath, cause.start, cause.end))
+    ParserError(s"$getMessage ${getStackTrace.toVector(0)}", pos)
+  }
+}
diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index 282bcf02e..b9468bd8a 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -11,7 +11,7 @@ import org.bitbucket.inkytonik.kiama.rewriting.{Cloner, PositionedRewriter, Stra
 import org.bitbucket.inkytonik.kiama.util.{Positions, Source}
 import org.bitbucket.inkytonik.kiama.util.Messaging.{error, message}
 import viper.gobra.ast.frontend._
-import viper.gobra.frontend.Source.{FromFileSource, TransformableSource, getPackageInfo}
+import viper.gobra.frontend.Source.{TransformableSource, getPackageInfo}
 import viper.gobra.reporting.{Source => _, _}
 import org.antlr.v4.runtime.{CharStreams, CommonTokenStream, DefaultErrorStrategy, ParserRuleContext}
 import org.antlr.v4.runtime.atn.PredictionMode
@@ -21,8 +21,8 @@ import scalaz.Scalaz.futureInstance
 import viper.gobra.frontend.GobraParser.{ExprOnlyContext, ImportDeclContext, MemberContext, PreambleContext, SourceFileContext, StmtOnlyContext, TypeOnlyContext}
 import viper.gobra.frontend.PackageResolver.{AbstractImport, AbstractPackage, BuiltInImport, RegularImport, RegularPackage}
 import viper.gobra.frontend.ParserUtils.ParseResult
-import viper.gobra.util.VerifierPhase.{ErrorsAndWarnings, PhaseResult, Warnings}
-import viper.gobra.util.{GobraExecutionContext, Job, TaskManager, VerifierPhaseNonFinal, Violation}
+import viper.gobra.util.VerifierPhase.PhaseResult
+import viper.gobra.util.{GobraExecutionContext, Job, TaskManager, VerifierPhase, VerifierPhaseNonFinal, Violation}
 import viper.silver.ast.SourcePosition
 
 import scala.collection.mutable.ListBuffer
@@ -31,8 +31,8 @@ import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap}
 import scala.concurrent.Future
 
 object ParserUtils {
-  type ParseSuccessResult = (Vector[Source], PPackage)
-  type ParseResult = Either[Vector[ParserError], ParseSuccessResult]
+  type ParseSuccessResult = (Vector[Source], PPackage, Vector[ParserWarning])
+  type ParseResult = Either[Vector[ParserMessage], ParseSuccessResult]
 }
 
 
@@ -41,8 +41,13 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
 
   override val name: String = "Parser"
 
-  type ImportToPkgInfoOrErrorMap = Vector[(AbstractPackage, Either[Vector[ParserError], (Vector[Source], PackageInfo)])]
+  private type ParserErrorsAndWarnings = Vector[ParserMessage]
+  private type ParserWarnings = Vector[ParserWarning]
+  type ImportToPkgInfoOrErrorMap = Vector[(AbstractPackage, Either[ParserErrorsAndWarnings, (Vector[Source], PackageInfo)])]
   type PreprocessedSources = Vector[Source]
+  private type PreambleResult = Either[ParserErrorsAndWarnings, (PPreamble, ParserWarnings)]
+  private type ProgramResult = Either[ParserErrorsAndWarnings, (PProgram, ParserWarnings)]
+  private type PackageResult = Either[ParserErrorsAndWarnings, (PPackage, ParserWarnings)]
 
   class ParseManager(config: Config)(implicit executor: GobraExecutionContext) extends LazyLogging {
     private val manager = new TaskManager[AbstractPackage, PreprocessedSources, ParseResult](config.parseAndTypeCheckMode)
@@ -63,18 +68,13 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       protected def getImports(importNodes: Vector[PImport], pom: PositionManager): ImportToPkgInfoOrErrorMap = {
         val explicitImports: Vector[(AbstractImport, ImportErrorFactory)] = importNodes
           .map(importNode => {
-            val importErrorFactory: ImportErrorFactory = (errMsg: String) => {
-              val err = pom.translate(message(importNode, errMsg), ParserError)
-              err
-            }
+            val importErrorFactory: ImportErrorFactory = (errMsg: String) =>
+              pom.translate(message(importNode, errMsg), ParserError)
             (RegularImport(importNode.importPath), importErrorFactory)
           })
         val imports = if (pkgInfo.isBuiltIn) { explicitImports } else {
-          val builtInImportErrorFactory: ImportErrorFactory = (errMsg: String) => {
-            val err = Vector(ParserError(errMsg, None))
-            config.reporter report ParserErrorMessage(err.head.position.get.file, err)
-            err
-          }
+          val builtInImportErrorFactory: ImportErrorFactory = (errMsg: String) =>
+            Vector(ParserError(errMsg, None))
           val builtInImportTuple = (BuiltInImport, builtInImportErrorFactory)
           explicitImports :+ builtInImportTuple
         }
@@ -107,11 +107,13 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       var preambleParsingDurationMs: Long = 0
 
       private def getImportsForPackage(preprocessedSources: Vector[Source]): ImportToPkgInfoOrErrorMap = {
-        val preambles = preprocessedSources
+        val preamblesAndWarnings = preprocessedSources
           .map(preprocessedSource => processPreamble(preprocessedSource)(config))
           // we ignore imports in files that cannot be parsed:
           .collect { case Right(p) => p }
-        preambles.flatMap(preamble => getImports(preamble.imports, preamble.positions))
+        preamblesAndWarnings.flatMap {
+          case (preamble, _) => getImports(preamble.imports, preamble.positions)
+        }
       }
 
       protected override def sequentialPrecompute(): PreprocessedSources = {
@@ -136,15 +138,16 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
         // introduce additional synchronization
         val startMs = System.currentTimeMillis()
         for {
-          parsedProgram <- Parser.process(preprocessedSources, pkgInfo, specOnly = specOnly)(config)
-          postprocessedProgram <- Parser.postprocess(Right((preprocessedSources, parsedProgram)), specOnly = specOnly)(config)
+          processResult <- Parser.process(preprocessedSources, pkgInfo, specOnly = specOnly)(config)
+          (parsedProgram, warnings) = processResult
+          postprocessedProgram <- Parser.postprocess(Right((preprocessedSources, parsedProgram, warnings)), specOnly = specOnly)(config)
           _ = logger.trace {
             val parsingDurationMs = System.currentTimeMillis() - startMs
             val parsingDurationS = f"${parsingDurationMs / 1000f}%.1f"
             val preambleParsingRatio = f"${100f * preambleParsingDurationMs / parsingDurationMs}%.1f"
             s"parsing ${pkgInfo.id} done (took ${parsingDurationS}s; parsing preamble overhead is ${preambleParsingRatio}%)"
           }
-        } yield (pkgSources, postprocessedProgram._2) // we use `pkgSources` as the preprocessing of sources should be transparent from the outside
+        } yield (pkgSources, postprocessedProgram._2, postprocessedProgram._3) // we use `pkgSources` as the preprocessing of sources should be transparent from the outside
       }
     }
 
@@ -160,7 +163,7 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       lazy val specOnly: Boolean = true
     }
 
-    private case class ParseFailureJob(errs: Vector[ParserError]) extends Job[PreprocessedSources, ParseResult] {
+    private case class ParseFailureJob(errs: ParserErrorsAndWarnings) extends Job[PreprocessedSources, ParseResult] {
       override protected def sequentialPrecompute(): PreprocessedSources =
         Vector.empty
       override protected def compute(precomputationResult: PreprocessedSources): ParseResult =
@@ -194,17 +197,33 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
     val (config, pkgInfo) = input
     val parseManager = new ParseManager(config)
     parseManager.parse(pkgInfo)
-    val res: Future[Either[ErrorsAndWarnings, (Map[AbstractPackage, ParseResult], Warnings)]] = for {
+    val res: Future[Either[ParserErrorsAndWarnings, (Map[AbstractPackage, ParseResult], ParserWarnings)]] = for {
       results <- parseManager.getResults
       res = results.get(RegularPackage(pkgInfo.id)) match {
-        case Some(Right(_)) => Right(results, Vector.empty)
-        case Some(Left(errs)) => Left(errs)
+        case Some(Right(pkgRes)) =>
+          report(config, pkgRes._3)
+          Right(results, pkgRes._3)
+        case Some(Left(errs)) =>
+          report(config, errs)
+          Left(errs)
         case _ => Violation.violation(s"No parse result for package '$pkgInfo' found")
       }
     } yield res
     EitherT.fromEither(res)
   }
 
+  private def report(config: Config, errorsAndWarnings: ParserErrorsAndWarnings): Unit = {
+    val groupedErrorsAndWarnings = errorsAndWarnings.groupBy{ _.position.get.file }
+    groupedErrorsAndWarnings.foreach { case (p, pErrorsAndWarnings) =>
+      val (pErrors, pWarnings) = VerifierPhase.splitErrorsAndWarnings(pErrorsAndWarnings)
+      if (pErrors.isEmpty) {
+        config.reporter report ParserSuccessMessage(p, pWarnings)
+      } else {
+        config.reporter report ParserFailureMessage(p, pErrors, pWarnings)
+      }
+    }
+  }
+
   private def preprocess(input: Vector[Source])(config: Config): Vector[Source] = {
     val sources = input.map(Gobrafier.gobrafy)
     sources.foreach { s => config.reporter report PreprocessedInputMessage(s.name, () => s.content) }
@@ -215,8 +234,8 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
     * Parses a source's preamble containing all (file-level) imports; This function expects that the input has already
     * been preprocessed
     */
-  private def processPreamble(preprocessedSource: Source)(config: Config): Either[Vector[ParserError], PPreamble] = {
-    def parseSource(preprocessedSource: Source): Either[Vector[ParserError], PPreamble] = {
+  private def processPreamble(preprocessedSource: Source)(config: Config): PreambleResult = {
+    def parseSource(preprocessedSource: Source): PreambleResult = {
       val positions = new Positions
       val pom = new PositionManager(positions)
       val parser = new SyntaxAnalyzer[PreambleContext, PPreamble](preprocessedSource, ListBuffer.empty[ParserError], pom, specOnly = true)
@@ -224,15 +243,15 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
     }
 
     var cacheHit: Boolean = true
-    def parseSourceCached(preprocessedSource: Source): Either[Vector[ParserError], PPreamble] = {
-      def parseAndStore(): Either[Vector[ParserError], PPreamble] = {
+    def parseSourceCached(preprocessedSource: Source): PreambleResult = {
+      def parseAndStore(): PreambleResult = {
         cacheHit = false
         parseSource(preprocessedSource)
       }
 
       val res = preambleCache.computeIfAbsent(getPreambleCacheKey(preprocessedSource), _ => parseAndStore())
       if (!cacheHit) {
-        logger.trace(s"No cache hit for ${res.map(_.packageClause.id.name)}'s preamble")
+        logger.trace(s"No cache hit for ${res.map(_._1.packageClause.id.name)}'s preamble")
       }
       res
     }
@@ -240,33 +259,40 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
     if (config.cacheParserAndTypeChecker) parseSourceCached(preprocessedSource) else parseSource(preprocessedSource)
   }
 
-  private def process(preprocessedInputs: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = {
+  private def process(preprocessedInputs: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): PackageResult = {
     parseSources(preprocessedInputs, pkgInfo, specOnly = specOnly)(config)
   }
 
-  private def postprocess(processResult: Either[Vector[ParserError], (Vector[Source], PPackage)], specOnly: Boolean)(config: Config): Either[Vector[ParserError], (Vector[Source], PPackage)] = {
+  private def postprocess(processResult: Either[ParserErrorsAndWarnings, (Vector[Source], PPackage, ParserWarnings)], specOnly: Boolean)(config: Config): Either[ParserErrorsAndWarnings, (Vector[Source], PPackage, ParserWarnings)] = {
     for {
       successfulProcessResult <- processResult
-      (preprocessedInputs, parseAst) = successfulProcessResult
+      (preprocessedInputs, parseAst, parseWarnings) = successfulProcessResult
       postprocessors = Seq(
         new ImportPostprocessor(parseAst.positions.positions),
         new TerminationMeasurePostprocessor(parseAst.positions.positions, specOnly = specOnly),
       )
-      postprocessedAst <- postprocessors.foldLeft[Either[Vector[ParserError], PPackage]](Right(parseAst)) {
-        case (Right(ast), postprocessor) => postprocessor.postprocess(ast)(config)
+      postprocessedAst <- postprocessors.foldLeft[Either[ParserErrorsAndWarnings, (PPackage, ParserWarnings)]](Right(parseAst, parseWarnings)) {
+        case (Right((ast, warnings)), postprocessor) => addWarnings(postprocessor.postprocess(ast)(config), warnings)
         case (e, _) => e
       }
-    } yield (preprocessedInputs, postprocessedAst)
+    } yield (preprocessedInputs, postprocessedAst._1, postprocessedAst._2)
+  }
+
+  private def addWarnings(result: PackageResult, warnings: ParserWarnings): PackageResult = {
+    result.fold(
+      errorsAndWarnings => Left(errorsAndWarnings ++ warnings),
+      pkgAndWarnings => Right(pkgAndWarnings._1, pkgAndWarnings._2 ++ warnings)
+    )
   }
 
   type SourceCacheKey = String
   // cache maps a key (obtained by hashing file path and file content) to the parse result
-  private val preambleCache: ConcurrentMap[SourceCacheKey, Either[Vector[ParserError], PPreamble]] = new ConcurrentHashMap()
+  private val preambleCache: ConcurrentMap[SourceCacheKey, PreambleResult] = new ConcurrentHashMap()
   type PackageCacheKey = String
   // we cache entire packages and not individual files (i.e. PProgram) as this saves us from copying over positional information
   // from one to the other position manager. Also, this transformation of copying positional information results in
   // differen PPackage instances that is problematic for caching type-check results.
-  private val packageCache: ConcurrentMap[PackageCacheKey, Either[Vector[ParserError], PPackage]] = new ConcurrentHashMap()
+  private val packageCache: ConcurrentMap[PackageCacheKey, PackageResult] = new ConcurrentHashMap()
 
   /** computes the key for caching the preamble of a particular source. This takes the name and the source's content into account */
   private def getPreambleCacheKey(source: Source): SourceCacheKey = {
@@ -289,8 +315,8 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
     packageCache.clear()
   }
 
-  private def parseSources(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = {
-    def parseSourcesCached(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = {
+  private def parseSources(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): PackageResult = {
+    def parseSourcesCached(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): PackageResult = {
       var cacheHit: Boolean = true
       val res = packageCache.computeIfAbsent(getPackageCacheKey(sources, pkgInfo, specOnly), _ => {
         cacheHit = false
@@ -307,18 +333,18 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
   }
 
   /** parses a package not taking the package cache but only the program cache into account */
-  private def parseSourcesUncached(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = {
+  private def parseSourcesUncached(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): PackageResult = {
     val positions = new Positions
     val pom = new PositionManager(positions)
     lazy val rewriter = new PRewriter(pom.positions)
 
-    def parseSource(source: Source): Either[Vector[ParserError], PProgram] = {
+    def parseSource(source: Source): ProgramResult = {
       val errors = ListBuffer.empty[ParserError]
       val parser = new SyntaxAnalyzer[SourceFileContext, PProgram](source, errors, pom, specOnly)
       parser.parse(parser.sourceFile) match {
-        case Right(ast) =>
+        case r@Right((ast, _)) =>
           config.reporter report ParsedInputMessage(source.name, () => ast)
-          Right(ast)
+          r
         case Left(errors) =>
           val (positionedErrors, nonpos) = errors.partition(_.position.nonEmpty)
           // Non-positioned errors imply some unexpected problems within the parser. We can't continue.
@@ -327,12 +353,16 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       }
     }
 
-    def isErrorFree(parserResults: Vector[Either[Vector[ParserError], PProgram]]): Either[Vector[ParserError], Vector[PProgram]] = {
-      val (errors, programs) = parserResults.partitionMap(identity)
-      if (errors.isEmpty) Right(programs) else Left(errors.flatten)
+    def isErrorFree(parserResults: Vector[ProgramResult]): Either[ParserErrorsAndWarnings, (Vector[PProgram], ParserWarnings)] = {
+      val (errorsAndWarnings, programsAndWarnings) = parserResults.partitionMap(identity)
+      if (errorsAndWarnings.isEmpty) Right(programsAndWarnings.foldLeft[(Vector[PProgram], ParserWarnings)]((Vector.empty, Vector.empty)) {
+        case ((prevProgs, prevWarnings), (prog, warnings)) => (prevProgs :+ prog, prevWarnings ++ warnings)
+      })
+      else Left(errorsAndWarnings.flatten)
     }
 
-    def checkPackageInfo(programs: Vector[PProgram]): Either[Vector[ParserError], Vector[PProgram]] = {
+    def checkPackageInfo(programsAndWarnings: (Vector[PProgram], ParserWarnings)): Either[ParserErrorsAndWarnings, (Vector[PProgram], ParserWarnings)] = {
+      val (programs, warnings) = programsAndWarnings
       require(programs.nonEmpty)
       val differingPkgNameMsgs = programs.flatMap(p =>
         error(
@@ -342,77 +372,70 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       )
 
       if (differingPkgNameMsgs.isEmpty) {
-        Right(programs)
+        Right(programs, warnings)
       } else {
-        Left(pom.translate(differingPkgNameMsgs, ParserError))
+        Left(pom.translate(differingPkgNameMsgs, ParserError) ++ warnings)
       }
     }
 
-    def makePackage(programs: Vector[PProgram]): Either[Vector[ParserError], PPackage] = {
+    def makePackage(programsAndWarnings: (Vector[PProgram], ParserWarnings)): PackageResult = {
+      val (programs, warnings) = programsAndWarnings
       val clause = rewriter.deepclone(programs.head.packageClause)
 
       val parsedPackage = PPackage(clause, programs, pom, pkgInfo)
 
       // The package parse tree node gets the position of the package clause:
       pom.positions.dupPos(clause, parsedPackage)
-      Right(parsedPackage)
+      Right(parsedPackage, warnings)
     }
 
     val parsedPrograms = sources.map(parseSource)
 
-    val res = for {
+    for {
       // check that each of the parsed programs has the same package clause. If not, the algorithm collecting all files
       // of the same package has failed or users have entered an invalid collection of inputs
-      programs <- isErrorFree(parsedPrograms)
-      programs <- checkPackageInfo(programs)
-      pkg <- makePackage(programs)
+      programsAndWarnings <- isErrorFree(parsedPrograms)
+      programsAndWarnings <- checkPackageInfo(programsAndWarnings)
+      pkg <- makePackage(programsAndWarnings)
     } yield pkg
-    // report potential errors:
-    res.left.foreach(errors => {
-      val groupedErrors = errors.groupBy{ _.position.get.file }
-      groupedErrors.foreach { case (p, pErrors) =>
-        config.reporter report ParserErrorMessage(p, pErrors)
-      }
-    })
-    res
   }
 
-  def parseProgram(source: Source, specOnly: Boolean = false): Either[Vector[ParserError], PProgram] = {
+  def parseProgram(source: Source, specOnly: Boolean = false): ProgramResult = {
     val positions = new Positions
     val pom = new PositionManager(positions)
     val parser = new SyntaxAnalyzer[SourceFileContext, PProgram](source, ListBuffer.empty[ParserError], pom, specOnly)
     parser.parse(parser.sourceFile())
   }
 
-  def parseMember(source: Source, specOnly: Boolean = false): Either[Vector[ParserError], Vector[PMember]] = {
+  def parseMember(source: Source, specOnly: Boolean = false): Either[ParserErrorsAndWarnings, (Vector[PMember], ParserWarnings)] = {
     val positions = new Positions
     val pom = new PositionManager(positions)
     val parser = new SyntaxAnalyzer[MemberContext, Vector[PMember]](source, ListBuffer.empty[ParserError], pom, specOnly)
     parser.parse(parser.member())
   }
 
-  def parseStmt(source: Source): Either[Vector[ParserError], PStatement] = {
+  def parseStmt(source: Source): Either[ParserErrorsAndWarnings, (PStatement, ParserWarnings)] = {
     val positions = new Positions
     val pom = new PositionManager(positions)
     val parser = new SyntaxAnalyzer[StmtOnlyContext, PStatement](source, ListBuffer.empty[ParserError], pom, false)
     parser.parse(parser.stmtOnly())
   }
 
-  def parseExpr(source: Source): Either[Vector[ParserError], PExpression] = {
+  def parseExpr(source: Source): Either[ParserErrorsAndWarnings, (PExpression, ParserWarnings)] = {
     val positions = new Positions
     val pom = new PositionManager(positions)
     val parser = new SyntaxAnalyzer[ExprOnlyContext, PExpression](source, ListBuffer.empty[ParserError], pom, false)
     parser.parse(parser.exprOnly())
   }
 
-  def parseImportDecl(source: Source): Either[Vector[ParserError], Vector[PImport]] = {
+  def parseImportDecl(source: Source): Either[ParserErrorsAndWarnings, (Vector[PImport], ParserWarnings)] = {
     val positions = new Positions
     val pom = new PositionManager(positions)
     val parser = new SyntaxAnalyzer[ImportDeclContext, Vector[PImport]](source, ListBuffer.empty[ParserError], pom, false)
     parser.parse(parser.importDecl())
   }
 
-  def parseType(source : Source) : Either[Vector[ParserError], PType] = {
+  def parseType(source : Source) : Either[ParserErrorsAndWarnings, (PType, ParserWarnings)] = {
     val positions = new Positions
     val pom = new PositionManager(positions)
     val parser = new SyntaxAnalyzer[TypeOnlyContext, PType](source, ListBuffer.empty[ParserError], pom, false)
@@ -428,18 +451,18 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       }
     }
 
-    def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage]
+    def postprocess(pkg: PPackage)(config: Config): PackageResult
   }
 
   private class ImportPostprocessor(override val positions: Positions) extends Postprocessor {
     /**
       * Replaces all PQualifiedWoQualifierImport by PQualifiedImport nodes
       */
-    def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] = {
+    def postprocess(pkg: PPackage)(config: Config): PackageResult = {
       def createError(n: PImplicitQualifiedImport, errorMsg: String): Vector[ParserError] = {
         val err = pkg.positions.translate(message(n,
           s"Explicit qualifier could not be derived (reason: '$errorMsg')"), ParserError)
-        config.reporter report ParserErrorMessage(err.head.position.get.file, err)
+        config.reporter report ParserFailureMessage(err.head.position.get.file, err, warnings = Vector.empty)
         err
       }
 
@@ -477,7 +500,7 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       // create a new package node with the updated programs
       val updatedPkg = PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg)
       // check whether an error has occurred
-      if (failedNodes.isEmpty) Right(updatedPkg)
+      if (failedNodes.isEmpty) Right(updatedPkg, Vector.empty)
       else Left(failedNodes)
     }
   }
@@ -494,11 +517,11 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       * Note that we do not transform the body of pure functions and pure methods (e.g. by turning the body into a
       * postcondition) because this would result in a matching loop for recursive functions.
       */
-    def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] = {
-      if (specOnly) replaceTerminationMeasures(pkg) else Right(pkg)
+    def postprocess(pkg: PPackage)(config: Config): PackageResult = {
+      if (specOnly) replaceTerminationMeasures(pkg) else Right(pkg, Vector.empty)
     }
 
-    private def replaceTerminationMeasures(pkg: PPackage): Either[Vector[ParserError], PPackage] = {
+    private def replaceTerminationMeasures(pkg: PPackage): PackageResult = {
       def replace(spec: PFunctionSpec): PFunctionSpec = {
         val replacedMeasures = spec.terminationMeasures.map {
           case n@PTupleTerminationMeasure(_, cond) => PWildcardMeasure(cond).at(n)
@@ -523,12 +546,12 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
         PProgram(prog.packageClause, prog.initPosts, prog.imports, updatedDecls).at(prog)
       })
       // create a new package node with the updated programs
-      Right(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg))
+      Right(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg), Vector.empty)
     }
   }
 
   private class SyntaxAnalyzer[Rule <: ParserRuleContext, Node <: AnyRef](tokens: CommonTokenStream, source: Source, errors: ListBuffer[ParserError], pom: PositionManager, specOnly: Boolean = false) extends GobraParser(tokens){
-
+    private type ParseResult = Either[ParserErrorsAndWarnings, (Node, ParserWarnings)]
 
     def this(source: Source, errors: ListBuffer[ParserError], pom: PositionManager, specOnly: Boolean) = {
       this({
@@ -581,7 +604,7 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
       res
     }
 
-    def parse(rule : => Rule): Either[Vector[ParserError], Node] = {
+    def parse(rule : => Rule): ParseResult = {
       val tree = try rule
       catch {
         case _: AmbiguityException => parse_LL(rule, overrideErrors = true) // Resolve `<IDENTIFIER> { }` ambiguities in switch/if-statements/closure-proofs
@@ -592,31 +615,16 @@ object Parser extends VerifierPhaseNonFinal[(Config, PackageInfo), Map[AbstractP
         val translator = new ParseTreeTranslator(pom, source, specOnly)
         val parseAst : Node = try translator.translate(tree)
           catch {
-            case e: TranslationFailure =>
-              val pos = source match {
-                case fileSource: FromFileSource => Some(SourcePosition(fileSource.path , e.cause.startPos.line, e.cause.endPos.column))
-                case _ => None
-              }
-              return Left(Vector(ParserError(e.getMessage + " " + e.getStackTrace.toVector(1), pos)))
-            case e: UnsupportedOperatorException =>
-              val pos = source match {
-                case fileSource: FromFileSource => Some(SourcePosition(fileSource.path, e.cause.startPos.line, e.cause.endPos.column))
-                case _ => None
-              }
-              return Left(Vector(ParserError(e.getMessage + " " + e.getStackTrace.toVector(0), pos)))
+            case e: TranslationException =>
+              return Left(Vector(e.toMessage(source)))
             case e: Throwable =>
-              val pos = source match {
-                case fileSource: FromFileSource => Some(SourcePosition(fileSource.path, 0, 0))
-                case _ => None
-              }
-              return Left(Vector(ParserError(e.getMessage + " " + e.getStackTrace.take(4).mkString("Array(", ", ", ")"), pos)))
+              val pos = Some(SourcePosition(source.toPath, 0, 0))
+              val errors = Vector(ParserError(e.getMessage + " " + e.getStackTrace.take(4).mkString("Array(", ", ", ")"), pos))
+              return Left(errors)
           }
 
-        // TODO : Add support for non-critical warnings in the verification process instead of printing them to stdout
-        if (translator.warnings.nonEmpty){
-          println(translator.warnings.mkString("Warnings: [", "\n" , " ]"))
-        }
-        Right(parseAst)
+        val warnings = translator.warnings.map(_.toMessage(source)).toVector
+        Right(parseAst, warnings)
       } else {
         Left(errors.toVector)
       }
diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala
index 8f92dd987..a8181ba1f 100644
--- a/src/main/scala/viper/gobra/frontend/info/Info.scala
+++ b/src/main/scala/viper/gobra/frontend/info/Info.scala
@@ -19,7 +19,7 @@ import viper.gobra.frontend.ParserUtils.{ParseResult, ParseSuccessResult}
 import viper.gobra.util.TaskManagerMode.{Lazy, Parallel, Sequential}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.typing.ghost.separation.{GhostLessPrinter, GoifyingPrinter}
-import viper.gobra.reporting.{CyclicImportError, NotFoundError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, TypeWarning, VerifierError}
+import viper.gobra.reporting.{CyclicImportError, NotFoundError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, TypeMessage, TypeWarning}
 import viper.gobra.util.VerifierPhase.{ErrorsAndWarnings, PhaseResult, Warnings}
 import viper.gobra.util.{GobraExecutionContext, Job, TaskManager, VerifierPhase, VerifierPhaseNonFinal, Violation}
 
@@ -34,9 +34,9 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
   override val name: String = "Type-checking"
 
   type GoTree = Tree[PNode, PPackage]
-  type TypeCheckSuccessResult = (TypeInfo with ExternalTypeInfo, Warnings)
-  type TypeCheckResult = Either[ErrorsAndWarnings, TypeCheckSuccessResult]
-  type DependentTypeCheckResult = Map[AbstractImport, TypeCheckResult]
+  private type TypeCheckSuccessResult = (TypeInfo with ExternalTypeInfo, Vector[TypeWarning])
+  private type TypeCheckResult = Either[Vector[TypeMessage], TypeCheckSuccessResult]
+  private type DependentTypeCheckResult = Map[AbstractImport, TypeCheckResult]
   type DependentTypeInfo = Map[AbstractImport, ExternalTypeInfo]
 
   trait GetParseResult {
@@ -61,7 +61,7 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
     def check(abstractPackage: AbstractPackage): Either[ErrorsAndWarnings, Map[AbstractPackage, ParseSuccessResult]] = {
       for {
         parseResult <- getParseResult(abstractPackage)
-        (_, ast) = parseResult
+        (_, ast, _) = parseResult
         perImportResult = ast.imports.map(importNode => {
           val res = getImportErrors(RegularImport(importNode.importPath))
             .left
@@ -82,12 +82,12 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
     /**
       * returns all parser errors and cyclic errors transitively found in imported packages
       */
-    private def getImportErrors(importTarget: AbstractImport): Either[Vector[VerifierError], Unit] = {
+    private def getImportErrors(importTarget: AbstractImport): Either[ErrorsAndWarnings, Unit] = {
       parserPendingPackages = parserPendingPackages :+ importTarget
       val abstractPackage = AbstractPackage(importTarget)(config)
       val res = for {
         parseResult <- getParseResult(abstractPackage)
-        (_, ast) = parseResult
+        (_, ast, _) = parseResult
         perImportResult = ast.imports.map(importNode => {
           val directlyImportedTarget = RegularImport(importNode.importPath)
           if (parserPendingPackages.contains(directlyImportedTarget)) {
@@ -106,13 +106,14 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
       res
     }
 
-    private def createImportError(importNode: PImport, errorsInImportedPackage: Vector[VerifierError]): Messages = {
-      val (cyclicErrors, nonCyclicErrors) = errorsInImportedPackage.partitionMap {
+    private def createImportError(importNode: PImport, errorsAndWarningsInImportedPackage: ErrorsAndWarnings): Messages = {
+      val (cyclicErrors, others) = errorsAndWarningsInImportedPackage.partitionMap {
         case cyclicErr: CyclicImportError => Left(cyclicErr)
         case e => Right(e)
       }
       if (cyclicErrors.isEmpty) {
-        message(importNode, s"Package contains ${nonCyclicErrors.length} error(s): ${nonCyclicErrors.map(_.message).mkString(", ")}")
+        val (errors, warnings) = VerifierPhase.splitErrorsAndWarnings(others)
+        message(importNode, s"Package contains ${errors.length} error(s) and ${warnings.length} warning(s): ${(errors ++ warnings).map(_.message).mkString(", ")}")
       } else {
         cyclicErrors.flatMap(cycle => message(importNode, cycle.message))
       }
@@ -140,7 +141,7 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
       override def toString: String = s"TypeCheckJob for $abstractPackage"
 
       protected override def sequentialPrecompute(): (Vector[Source], PPackage, Vector[AbstractImport]) = {
-        val (sources, ast) = getParseResult(abstractPackage)
+        val (sources, ast, _) = getParseResult(abstractPackage)
         val importTargets = ast.imports.map(importNode => RegularImport(importNode.importPath))
         val isBuiltIn = abstractPackage == BuiltInPackage
         val dependencies = if (isBuiltIn) importTargets else BuiltInImport +: importTargets
@@ -205,13 +206,15 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
       // check whether there are any import cycles:
       cycleResult <- EitherT.fromEither(Future.successful(new CycleChecker(config, parseResults).check(abstractPackage)))
         .leftMap(errorsAndWarnings => {
-          val (sources, pkg) = parseResult
+          val (sources, pkg, _) = parseResult
           reportTypeCheckFailure(config, sources, pkg, errorsAndWarnings)
           errorsAndWarnings
         })
       typeCheckingStartMs = System.currentTimeMillis()
       context = new Context(config, cycleResult)
-      typeInfo <- EitherT.fromEither(context.typeCheck(abstractPackage))
+      // the following type annotation is necessary to overcome an incompleteness of Scala's type checker:
+      typeCheckRes: Future[Either[ErrorsAndWarnings, (TypeInfo, Warnings)]] = context.typeCheck(abstractPackage)
+      typeInfo <- EitherT.fromEither(typeCheckRes)
       _ = logger.debug {
         val typeCheckingEndMs = System.currentTimeMillis()
         val sumDurationS = f"${context.typeCheckDurationMs.get() / 1000f}%.1f"
@@ -351,7 +354,7 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
     }
   }
 
-  private def convertToTypeErrorsAndWarnings(pkg: PPackage, msgs: Messages): Either[ErrorsAndWarnings, Warnings] = {
+  private def convertToTypeErrorsAndWarnings(pkg: PPackage, msgs: Messages): Either[Vector[TypeMessage], Vector[TypeWarning]] = {
     val (warningMsgs, errorMsgs) = msgs.partition(_.severity == Severities.Warning)
 
     // the type checker sometimes produces duplicate errors, which we remove here (e.g., when type checking
diff --git a/src/main/scala/viper/gobra/reporting/Message.scala b/src/main/scala/viper/gobra/reporting/Message.scala
index d6ecdb5a2..beef4f2d0 100644
--- a/src/main/scala/viper/gobra/reporting/Message.scala
+++ b/src/main/scala/viper/gobra/reporting/Message.scala
@@ -103,12 +103,21 @@ case class ParsedInputMessage(input: String, ast: () => PProgram) extends GobraM
     s"file=$input)"
 }
 
-case class ParserErrorMessage(input: Path, result: Vector[ParserError]) extends GobraMessage {
-  override val name: String = s"parser_error_message"
+case class ParserSuccessMessage(input: Path, warnings: Vector[ParserWarning]) extends GobraMessage {
+  override val name: String = s"parser_success_message"
 
-  override def toString: String = s"parser_error_message(" +
-    s"file=$input), " +
-    s"errors=${result.map(_.toString).mkString(",")})"
+  override def toString: String = s"parser_success_message(" +
+    s"file=$input, " +
+    s"warnings=${warnings.map(_.toString).mkString(",")})"
+}
+
+case class ParserFailureMessage(input: Path, errors: Vector[ParserError], warnings: Vector[ParserWarning]) extends GobraMessage {
+  override val name: String = s"parser_failure_message"
+
+  override def toString: String = s"parser_failure_message(" +
+    s"file=$input, " +
+    s"errors=${errors.map(_.toString).mkString(",")}, " +
+    s"warnings=${warnings.map(_.toString).mkString(",")})"
 }
 
 sealed trait TypeCheckMessage extends GobraMessage {
diff --git a/src/main/scala/viper/gobra/reporting/Reporter.scala b/src/main/scala/viper/gobra/reporting/Reporter.scala
index f3707e5f3..847416213 100644
--- a/src/main/scala/viper/gobra/reporting/Reporter.scala
+++ b/src/main/scala/viper/gobra/reporting/Reporter.scala
@@ -67,8 +67,14 @@ case class FileWriterReporter(name: String = "filewriter_reporter",
         errors.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
       case _ => // ignore
     }
-    case m:ParserErrorMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
-    case m:TypeCheckFailureMessage if streamErrs =>
+    case m: ParserSuccessMessage if streamErrs =>
+      m.warnings.foreach(warning => logger.warn(s"Warning at: ${warning.formattedMessage}"))
+    case m: ParserFailureMessage if streamErrs =>
+      m.warnings.foreach(warning => logger.warn(s"Warning at: ${warning.formattedMessage}"))
+      m.errors.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
+    case m: TypeCheckSuccessMessage if streamErrs =>
+      m.warnings.foreach(warning => logger.warn(s"Warning at: ${warning.formattedMessage}"))
+    case m: TypeCheckFailureMessage if streamErrs =>
       m.warnings.foreach(warning => logger.warn(s"Warning at: ${warning.formattedMessage}"))
       m.errors.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
     case m:TransformerFailureMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
diff --git a/src/main/scala/viper/gobra/reporting/VerifierMessage.scala b/src/main/scala/viper/gobra/reporting/VerifierMessage.scala
index 8a6d86050..17a9775c7 100644
--- a/src/main/scala/viper/gobra/reporting/VerifierMessage.scala
+++ b/src/main/scala/viper/gobra/reporting/VerifierMessage.scala
@@ -35,10 +35,6 @@ sealed trait VerifierWarning extends VerifierMessage {
   override def severity: Severity = Severities.Warning
 }
 
-case class TypeWarning(message: String, position: Option[SourcePosition]) extends VerifierWarning {
-  val id = "type_warning"
-}
-
 sealed trait VerifierError extends VerifierMessage {
   override def severity: Severity = Severities.Error
 }
@@ -53,11 +49,23 @@ case class ConfigError(message: String) extends VerifierError {
   val id = "config_error"
 }
 
-case class ParserError(message: String, position: Option[SourcePosition]) extends VerifierError {
+sealed trait ParserMessage extends VerifierMessage
+
+case class ParserWarning(message: String, position: Option[SourcePosition]) extends ParserMessage with VerifierWarning {
+  val id = "parser_warning"
+}
+
+case class ParserError(message: String, position: Option[SourcePosition]) extends ParserMessage with VerifierError {
   val id = "parser_error"
 }
 
-case class TypeError(message: String, position: Option[SourcePosition]) extends VerifierError {
+sealed trait TypeMessage extends VerifierMessage
+
+case class TypeWarning(message: String, position: Option[SourcePosition]) extends TypeMessage with VerifierWarning {
+  val id = "type_warning"
+}
+
+case class TypeError(message: String, position: Option[SourcePosition]) extends TypeMessage with VerifierError {
   val id = "type_error"
 }
 
diff --git a/src/main/scala/viper/gobra/util/VerifierPhase.scala b/src/main/scala/viper/gobra/util/VerifierPhase.scala
index 004b746b6..4e2b4893e 100644
--- a/src/main/scala/viper/gobra/util/VerifierPhase.scala
+++ b/src/main/scala/viper/gobra/util/VerifierPhase.scala
@@ -10,7 +10,7 @@ import scala.concurrent.Future
 import com.typesafe.scalalogging.LazyLogging
 import scalaz.EitherT
 import scalaz.Scalaz.futureInstance
-import viper.gobra.reporting.{VerifierError, VerifierMessage, VerifierResult, VerifierWarning}
+import viper.gobra.reporting.{ParserError, ParserMessage, ParserWarning, TypeError, TypeMessage, TypeWarning, VerifierError, VerifierMessage, VerifierResult, VerifierWarning}
 import viper.gobra.util.VerifierPhase.PhaseResult
 
 object VerifierPhase {
@@ -18,11 +18,34 @@ object VerifierPhase {
   type Warnings = Vector[VerifierWarning]
   type PhaseResult[S] = EitherT[ErrorsAndWarnings, Future, (S, Warnings)]
 
-  def splitErrorsAndWarnings(i: ErrorsAndWarnings): (Vector[VerifierError], Warnings) =
-    i.partitionMap {
-      case e: VerifierError => Left(e)
-      case w: VerifierWarning => Right(w)
+  trait Splitter[M <: VerifierMessage, E <: VerifierError, W <: VerifierWarning] {
+    def split(msg: M): Either[E, W]
+  }
+
+  object Splitter {
+    implicit object VerifierSplitter extends Splitter[VerifierMessage, VerifierError, VerifierWarning] {
+      override def split(msg: VerifierMessage): Either[VerifierError, VerifierWarning] = msg match {
+        case e: VerifierError => Left(e)
+        case w: VerifierWarning => Right(w)
+      }
+    }
+    implicit object ParserSplitter extends Splitter[ParserMessage, ParserError, ParserWarning] {
+      override def split(msg: ParserMessage): Either[ParserError, ParserWarning] = msg match {
+        case e: ParserError => Left(e)
+        case w: ParserWarning => Right(w)
+      }
     }
+    implicit object TypeSplitter extends Splitter[TypeMessage, TypeError, TypeWarning] {
+      override def split(msg: TypeMessage): Either[TypeError, TypeWarning] = msg match {
+        case e: TypeError => Left(e)
+        case w: TypeWarning => Right(w)
+      }
+    }
+  }
+
+  def splitErrorsAndWarnings[M <: VerifierMessage, E <: VerifierError, W <: VerifierWarning](i: Vector[M])(implicit splitter: Splitter[M, E, W]): (Vector[E], Vector[W]) = {
+    i.partitionMap { splitter.split }
+  }
 }
 
 trait VerifierPhase[I, R] extends LazyLogging {
diff --git a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala
index 9f6cf272b..85b49ac00 100644
--- a/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala
+++ b/src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala
@@ -376,7 +376,7 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
       // try to parse ghostLess string:
       val parseRes = Parser.parseProgram(StringSource(ghostLess, "Ghostless Program"), false)
       parseRes match {
-        case Right(prog) => prog
+        case Right((prog, _)) => prog
         case Left(messages) => fail(s"Parsing failed: $messages")
       }
     }
@@ -415,12 +415,12 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
     def testProg(inputProg: String, expectedErasedProg: String): Assertion = {
       val inputParseAst = Parser.parseProgram(StringSource(inputProg, "Input Program"))
       val ghostlessProg = inputParseAst match {
-        case Right(prog) => ghostLessProg(prog)
+        case Right((prog, _)) => ghostLessProg(prog)
         case Left(msgs) => fail(s"Parsing input program has failed with $msgs")
       }
       val expectedParseAst = Parser.parseProgram(StringSource(expectedErasedProg, "Expected Program"))
       expectedParseAst match {
-        case Right(prog) => equal(ghostlessProg, prog)
+        case Right((prog, _)) => equal(ghostlessProg, prog)
         case Left(msgs) => fail(s"Parsing expected erased program has failed with $msgs")
       }
     }
diff --git a/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala b/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala
index e9699c2e4..7e8bc393f 100644
--- a/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala
+++ b/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala
@@ -10,15 +10,18 @@ import org.bitbucket.inkytonik.kiama.util.{Source, StringSource}
 import org.scalatest.Assertions.fail
 import viper.gobra.ast.frontend.{PExpression, PImport, PMember, PProgram, PStatement, PType}
 import viper.gobra.frontend.Parser
-import viper.gobra.reporting.ParserError
+import viper.gobra.reporting.{ParserError, ParserMessage, ParserWarning}
 
 import scala.reflect.ClassTag
 
 class ParserTestFrontend {
-  private def parse[T: ClassTag](source: String, parser: Source => Either[Vector[ParserError], T]) : Either[Vector[ParserError], T] =
-    parser(StringSource(source))
+  private def parse[T: ClassTag](source: String, parser: Source => Either[Vector[ParserMessage], (T, Vector[ParserWarning])]) : Either[Vector[ParserError], T] =
+    parser(StringSource(source)).fold(
+      messages => Left(messages.collect { case e: ParserError => e }),
+      { case (ast, _) => Right(ast) }
+    )
 
-  private def parseOrFail[T: ClassTag](source: String, parser: Source => Either[Vector[ParserError], T]): T = {
+  private def parseOrFail[T: ClassTag](source: String, parser: Source => Either[Vector[ParserMessage], (T, Vector[ParserWarning])]): T = {
     parse(source, parser) match {
       case Right(ast) => ast
       case Left(messages) => fail(s"Parsing failed: $messages")