diff --git a/src/main/scala/viper/silver/frontend/ReformatterAstProvider.scala b/src/main/scala/viper/silver/frontend/ReformatterAstProvider.scala
new file mode 100644
index 000000000..be275678e
--- /dev/null
+++ b/src/main/scala/viper/silver/frontend/ReformatterAstProvider.scala
@@ -0,0 +1,26 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2024 ETH Zurich.
+
+package viper.silver.frontend
+import viper.silver.parser.PProgram
+import viper.silver.reporter.Reporter
+import viper.silver.verifier.{Failure, Success, VerificationResult}
+
+class ReformatterAstProvider(override val reporter: Reporter) extends ViperAstProvider(reporter) {
+  override val phases: Seq[Phase] = Seq(Parsing)
+
+  override def doParsing(input: String): Result[PProgram] = parsingInner(input, false)
+
+  override def result: VerificationResult = {
+    if (_errors.isEmpty) {
+      require(state >= DefaultStates.Parsing)
+      Success
+    }
+    else {
+      Failure(_errors)
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index 5de692857..55283c9ce 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -310,11 +310,11 @@ trait SilFrontend extends DefaultFrontend {
     _config = configureVerifier(args)
   }
 
-  override def doParsing(input: String): Result[PProgram] = {
+  def parsingInner(input: String, expandMacros: Boolean): Result[PProgram] = {
     val file = _inputFile.get
     plugins.beforeParse(input, isImported = false) match {
       case Some(inputPlugin) =>
-        val result = fp.parse(inputPlugin, file, Some(plugins), _loader)
+        val result = fp.parse(inputPlugin, file, Some(plugins), _loader, expandMacros)
         if (result.errors.forall(p => p.isInstanceOf[ParseWarning])) {
           reporter report WarningsDuringParsing(result.errors)
           Succ({
@@ -327,6 +327,8 @@ trait SilFrontend extends DefaultFrontend {
     }
   }
 
+  override def doParsing(input: String): Result[PProgram] = parsingInner(input, true)
+
   override def doSemanticAnalysis(input: PProgram): Result[PProgram] = {
     plugins.beforeResolve(input) match {
       case Some(inputPlugin) =>
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index eae845045..8d8106c50 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -27,13 +27,26 @@ object FastParserCompanion {
   val whitespaceWithoutNewlineOrComments = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
-      NoTrace((" " | "\t").rep)
+      NoTrace(space.rep)
   }
 
+  def blockComment[$: P] = {
+    import NoWhitespace._
+    "/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/"
+  }
+
+  def lineComment[$: P] = {
+    import NoWhitespace._
+    "//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)
+  }
+
+  def space[$: P] = " " | "\t"
+  def newline[$: P] = StringIn("\r\n") | "\n" | "\r"
+
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      NoTrace((blockComment | lineComment | space | newline).rep)
   }
 
   def identStarts[$: P] = CharIn("A-Z", "a-z", "$_")
@@ -104,6 +117,27 @@ object FastParserCompanion {
       ).pos
   }
 
+  /* These special parser methods are only used in the reformatter
+  to parse and interpret the whitespaces and comments between two AST nodes.
+  */
+  def pSpace[$: P]: P[PSpace] = P(space map (_ => PSpace()))
+
+  def pNewline[$: P]: P[PNewLine] = P(newline map (_ => PNewLine()))
+
+  def pLineComment[$: P]: P[PComment] = P(lineComment.!.map { content =>
+    PComment(content)
+  })
+
+  def pBlockComment[$: P]: P[PComment] = P(blockComment.!.map { content =>
+    PComment(content)
+  })
+
+  def pComment[$: P]: P[PComment] = pLineComment | pBlockComment
+
+  def pTrivia[$: P]: P[Seq[PTrivia]] = {
+    P((pSpace | pNewline | pComment).repX)
+  }
+
   /**
     * A parser which matches leading whitespaces. See `LeadingWhitespace.lw` for more info. Can only be operated on in
     * restricted ways (e.g. `?`, `rep`, `|` or `map`), requiring that it is eventually appended to a normal parser (of type `P[V]`).
@@ -167,7 +201,7 @@ object FastParserCompanion {
 }
 
 class FastParser {
-  def parse(s: String, f: Path, plugins: Option[SilverPluginManager] = None, loader: FileLoader = DiskLoader) = {
+  def parse(s: String, f: Path, plugins: Option[SilverPluginManager] = None, loader: FileLoader = DiskLoader, expandMacros: Boolean = true) = {
     // Strategy to handle imports
     // Idea: Import every import reference and merge imported methods, functions, imports, .. into current program
     //       iterate until no new imports are present.
@@ -179,7 +213,11 @@ class FastParser {
     val file = f.toAbsolutePath().normalize()
     val data = ParserData(plugins, loader, mutable.HashSet(file))
     val program = RecParser(file, data, false).parses(s)
-    MacroExpander.expandDefines(program)
+    if (expandMacros) {
+      MacroExpander.expandDefines(program)
+    } else  {
+      program
+    }
   }
 
   case class ParserData(plugins: Option[SilverPluginManager], loader: FileLoader, local: mutable.HashSet[Path], std: mutable.HashSet[Path] = mutable.HashSet.empty)
@@ -312,13 +350,13 @@ class FastParser {
   //////////////////////////
 
   import fastparse._
-  import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym}
+  import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym, blockComment, lineComment, newline, space}
 
 
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      NoTrace((blockComment | lineComment | space | newline).rep)
   }
 
   implicit val lineCol: LineCol = new LineCol(this)
@@ -859,7 +897,7 @@ class FastParser {
     P(programMember.rep map (members => {
       val warnings = _warnings
       _warnings = Seq()
-      PProgram(Nil, members)(_, warnings)
+      PProgram(Nil, members)(_, warnings, Nil, "")
     })).pos
 
   def preambleImport[$: P]: P[PKw.Import => PAnnotationsPosition => PImport] = P(
@@ -886,7 +924,7 @@ class FastParser {
       val axioms1 = members collect { case m: PAxiom1 => m }
       val funcs = funcs1 map (f => (PDomainFunction(f.annotations, f.unique, f.function, f.idndef, f.args, f.c, f.typ, f.interpretation)(f.pos), f.s))
       val axioms = axioms1 map (a => (PAxiom(a.annotations, a.axiom, a.idndef, a.exp)(a.pos), a.s))
-      val allMembers = block.update(PDomainMembers(PDelimited(funcs)(NoPosition, NoPosition), PDelimited(axioms)(NoPosition, NoPosition))(block.pos))
+      val allMembers = block.update(PDomainMembers(PDelimited(funcs)(NoPosition, NoPosition), PDelimited(axioms)(NoPosition, NoPosition))(block.pos, block.inner))
       k => ap: PAnnotationsPosition => PDomain(
         ap.annotations,
         k,
@@ -970,7 +1008,11 @@ class FastParser {
 
     // Assume entire file is correct and try parsing it quickly
     fastparse.parse(s, entireProgram(_)) match {
-      case Parsed.Success(value, _) => return value
+      case Parsed.Success(value, _) => {
+        value.offsets = _line_offset;
+        value.rawProgram = s;
+        return value;
+      }
       case _: Parsed.Failure =>
     }
     // There was a parsing error, parse member by member to get all errors
@@ -1018,7 +1060,7 @@ class FastParser {
     val warnings = _warnings
     _warnings = Nil
     val pos = (FilePosition(lineCol.getPos(0)), FilePosition(lineCol.getPos(res.get.index)))
-    PProgram(Nil, members)(pos, errors ++ warnings)
+    PProgram(Nil, members)(pos, errors ++ warnings, Nil, "");
   }
 
   object ParserExtension extends ParserPluginTemplate {
diff --git a/src/main/scala/viper/silver/parser/MacroExpander.scala b/src/main/scala/viper/silver/parser/MacroExpander.scala
index 0a5bcfee9..6419a934d 100644
--- a/src/main/scala/viper/silver/parser/MacroExpander.scala
+++ b/src/main/scala/viper/silver/parser/MacroExpander.scala
@@ -156,9 +156,9 @@ object MacroExpander {
                 pos._1
             }
           }
-          return PProgram(newImported, program.members)(program.pos, program.localErrors ++ reports :+ ParseError(msg, location))
+          return PProgram(newImported, program.members)(program.pos, program.localErrors ++ reports :+ ParseError(msg, location), program.offsets, program.rawProgram)
       }
-      PProgram(newImported, newMembers)(program.pos, program.localErrors ++ reports)
+      PProgram(newImported, newMembers)(program.pos, program.localErrors ++ reports, program.offsets, program.rawProgram)
     }
 
     doExpandDefinesAll(p, reports)
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 9f2134825..ab6d6dd84 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -8,8 +8,11 @@ package viper.silver.parser
 
 import java.util.concurrent.atomic.{AtomicInteger, AtomicLong}
 import viper.silver.ast.utility.Visitor
-import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, HasExtraVars, HasExtraValList}
+import viper.silver.ast.utility.rewriter.{HasExtraValList, HasExtraVars, Rewritable, StrategyBuilder}
 import viper.silver.ast.{Exp, FilePosition, HasLineColumn, Member, NoPosition, Position, SourcePosition, Stmt, Type}
+import viper.silver.parser.ReformatPrettyPrinter.{show, showAnnotations, showBody, showInvs, showNestedPaddedExpr, showOption, showPresPosts, showReturns, showSeq}
+import viper.silver.parser.PSymOp.{EqEq, Iff, Implies}
+import viper.silver.parser.RNode._
 import viper.silver.parser.TypeHelper._
 import viper.silver.verifier.ParseReport
 
@@ -30,11 +33,19 @@ trait Where {
   * The root of the parser abstract syntax tree.  Note that we prefix all nodes with `P` to avoid confusion
   * with the actual Viper abstract syntax tree.
   */
-trait PNode extends Where with Product with Rewritable with HasExtraValList {
+trait PNode extends Where with Product with Rewritable with HasExtraValList with Reformattable {
 
   /* Should output something that can be displayed to the user. */
   def pretty: String
 
+  // By default, we can fall back to the `pretty` implementation, for any case where we just
+  // need to show keywords or single tokens. But as soon as we need to add whitespaces,
+  // we will have to override this
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = this match {
+    case p: PLeaf => rt(p.pretty)
+    case _ => ReformatPrettyPrinter.reformatNodesNoSpace(this)
+  }
+
   /** Returns a list of all direct sub-nodes of this node. */
   def subnodes: Seq[PNode] = PNode.children(this, this).flatMap(PNode.nodes(this, _)).toSeq
 
@@ -627,13 +638,18 @@ case class PFunctionType(argTypes: Seq[PType], resultType: PType) extends PInter
     val argsPretty = argTypes.map(_.pretty).mkString("(", ", ", ")")
     s"$argsPretty: ${resultType.pretty}"
   }
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    rt("(") <> argTypes.map(show(_)).reduce(_ <> rt(", ") <> _) <> rt(")") <>
+    rt(": ") <> show(resultType)
+  }
 }
 
 ///////////////////////////////////////////////////////////////////////////////////////
 // Expressions
 // typeSubstitutions are the possible substitutions used for type checking and inference
 // The argument types are unified with the (fresh versions of) types  are
-trait PExp extends PNode with PPrettySubnodes {
+trait PExp extends PNode with PPrettySubnodes with ReformattableExpression {
   var brackets: Option[PGrouped.Paren[PExp]] = None
   var typ: PType = PUnknown()
 
@@ -654,6 +670,27 @@ trait PExp extends PNode with PPrettySubnodes {
     case Some(b) => s"${b.l.pretty}${super.pretty}${b.r.pretty}"
     case None => super.pretty
   }
+
+  // Note: We override the `reformat` for all expressions here, classes implementing this trait
+  // should not override it. Instead, they should implement the `reformatExp` method.
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    // Unfortunately, we cannot just show exp.brackets, because then we end up in an
+    // endless recursion. So instead, we need to add them manually.
+    brackets match {
+      case Some(b) => {
+        if (b.l.isInstanceOf[PSym.Brace]) {
+          // Braced expressions should either be in the same line but with a space padding
+          // (e.g. { var i := 1; }), or be broken into the next line if too long.
+          rne(rg(show(b.l) <@> this.reformatExp(ctx) <@> show(b.r)))
+        } else {
+          // We don't want i <= (n + 1) to turn into
+          // i <= ( n + 1 ), for example.
+          show(b.l) <> this.reformatExp(ctx) <> show(b.r)
+        }
+      }
+      case None => this.reformatExp(ctx)
+    }
+  }
 }
 
 case class PAnnotatedExp(annotation: PAnnotation, e: PExp)(val pos: (Position, Position)) extends PExp {
@@ -996,6 +1033,16 @@ class PBinExp(val left: PExp, val op: PReserved[PBinaryOp], val right: PExp)(val
 
   override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(left, op.rs.operator, right)
   override def toString(): String = s"PBinExp($left,$op,$right)"
+
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = {
+    op.rs match {
+      // Those operators look a bit better if they stick on the previous line
+      case Iff | Implies | EqEq =>
+        rg(show(left) <+> show(op) <> rne(rl() <> show(right)))
+      case _ => rg(show(left) <@> show(op) <+> show(right))
+    }
+
+  }
 }
 
 object PBinExp {
@@ -1017,6 +1064,10 @@ case class PCondExp(cond: PExp, q: PSymOp.Question, thn: PExp, c: PSymOp.Colon,
   val signatures: List[PTypeSubstitution] = List(
     Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(2) -> POpApp.pArg(1), POpApp.pResS -> POpApp.pArg(1))
   )
+
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = show(cond) <+> show(q) <>
+    rne(rg(rl() <> show(thn) <+>
+      show(c) <> rg(rl() <> show(els))))
 }
 
 // Simple literals
@@ -1072,18 +1123,26 @@ case class PUnfolding(unfolding: PKwOp.Unfolding, acc: PAccAssertion, in: PKwOp.
   override val args = Seq(acc, exp)
   override val signatures: List[PTypeSubstitution] =
     List(Map(POpApp.pArgS(0) -> Predicate, POpApp.pResS -> POpApp.pArg(1)))
+
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = show(unfolding) <> show(acc) <+> show(in) <> showNestedPaddedExpr(exp)
 }
 
 case class PApplying(applying: PKwOp.Applying, wand: PExp, in: PKwOp.In, exp: PExp)(val pos: (Position, Position)) extends PHeapOpApp {
   override val args = Seq(wand, exp)
   override val signatures: List[PTypeSubstitution] =
     List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
+
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = show(applying) <> show(wand) <+> show(in) <> showNestedPaddedExpr(exp)
 }
 
 case class PAsserting(asserting: PKwOp.Asserting, a: PExp, in: PKwOp.In, exp: PExp)(val pos: (Position, Position)) extends PHeapOpApp {
   override val args = Seq(a, exp)
   override val signatures: List[PTypeSubstitution] =
     List(Map(POpApp.pArgS(0) -> Impure, POpApp.pResS -> POpApp.pArg(1)))
+
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = show(asserting) <>
+    rne(rg(rl() <> show(a))) <+>
+    show(in) <> showNestedPaddedExpr(exp)
 }
 
 sealed trait PBinder extends PExp with PScope {
@@ -1114,12 +1173,22 @@ sealed trait PQuantifier extends PBinder {
   override def boundVars = vars.toSeq
 }
 
-case class PExists(keyword: PKw.Exists, vars: PDelimited[PLogicalVarDecl, PSym.Comma], c: PSym.ColonColon, triggers: Seq[PTrigger], body: PExp)(val pos: (Position, Position)) extends PQuantifier
+case class PExists(keyword: PKw.Exists, vars: PDelimited[PLogicalVarDecl, PSym.Comma], c: PSym.ColonColon, triggers: Seq[PTrigger], body: PExp)(val pos: (Position, Position)) extends PQuantifier {
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = show(keyword) <> show(vars) <>
+    show(c) <> rne(rg(rl() <> (showSeq(triggers) <+> show(body))))
+}
 
-case class PForall(keyword: PKw.Forall, vars: PDelimited[PLogicalVarDecl, PSym.Comma], c: PSym.ColonColon, triggers: Seq[PTrigger], body: PExp)(val pos: (Position, Position)) extends PQuantifier
+case class PForall(keyword: PKw.Forall, vars: PDelimited[PLogicalVarDecl, PSym.Comma], c: PSym.ColonColon, triggers: Seq[PTrigger], body: PExp)(val pos: (Position, Position)) extends PQuantifier {
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = show(keyword) <> show(vars) <>
+    show(c) <> rne(rg(rl() <> rg(showSeq(triggers) <+> show(body))))
+}
 
 case class PForPerm(keyword: PKw.Forperm, vars: PDelimited[PLogicalVarDecl, PSym.Comma], accessRes: PGrouped[PSym.Bracket, PResourceAccess], c: PSym.ColonColon, body: PExp)(val pos: (Position, Position)) extends PQuantifier {
   val triggers: Seq[PTrigger] = Seq()
+
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = show(keyword) <>
+    show(vars) <+> show(accessRes) <> show(c) <>
+    rne(rg(rl() <> show(body)))
 }
 
 /* Let-expressions `let x == e1 in e2` are represented by the nested structure
@@ -1142,6 +1211,9 @@ case class PLet(l: PKwOp.Let, variable: PIdnDef, eq: PSymOp.EqEq, exp: PGrouped.
     nestedScope.body.forceSubstitution(ts)
     typ = nestedScope.body.typ
   }
+
+  override def reformatExp(implicit ctx: ReformatterContext): List[RNode] = show(l) <> show(variable) <+>
+    show(eq) <+> show(exp) <+> show(in) <> rg(rl() <> show(nestedScope))
 }
 
 case class PLetNestedScope(body: PExp)(val pos: (Position, Position)) extends PTypedVarDecl with PLocalDeclaration with PScopeUniqueDeclaration {
@@ -1342,7 +1414,6 @@ sealed trait PSetLiteral extends PCollectionLiteral {
 case class PEmptySet(op: PKwOp.Set, pAnnotatedType: Option[PGrouped[PSym.Bracket, PType]], callArgs: PDelimited.Comma[PSym.Paren, Nothing])(val pos: (Position, Position)) extends PSetLiteral with PEmptyCollectionLiteral
 
 case class PExplicitSet(op: PKwOp.Set, callArgs: PDelimited.Comma[PSym.Paren, PExp])(val pos: (Position, Position)) extends PSetLiteral with PExplicitCollectionLiteral
-
 sealed trait PMultiSetLiteral extends PCollectionLiteral {
   def pCollectionType(pType: PType) = if (pType.isUnknown) PUnknown() else MakeMultiset(pType)
 }
@@ -1432,7 +1503,9 @@ case class PMapRange(keyword: PKwOp.Range, base: PGrouped.Paren[PExp])(val pos:
 
 ///////////////////////////////////////////////////////////////////////////
 // Statements
-trait PStmt extends PNode with PPrettySubnodes
+trait PStmt extends PNode with PPrettySubnodes {
+  // Most statements are just separated by spaces, so we override the default here.
+}
 
 case class PAnnotatedStmt(annotation: PAnnotation, stmt: PStmt)(val pos: (Position, Position)) extends PStmt
 
@@ -1452,7 +1525,9 @@ case class PFold(fold: PKw.Fold, e: PExp)(val pos: (Position, Position)) extends
 
 case class PUnfold(unfold: PKw.Unfold, e: PExp)(val pos: (Position, Position)) extends PStmt
 
-case class PPackageWand(pckg: PKw.Package, e: PExp, proofScript: Option[PSeqn])(val pos: (Position, Position)) extends PStmt
+case class PPackageWand(pckg: PKw.Package, e: PExp, proofScript: Option[PSeqn])(val pos: (Position, Position)) extends PStmt {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = show(pckg) <> show(e) <+> showOption(proofScript)
+}
 
 case class PApplyWand(apply: PKw.Apply, e: PExp)(val pos: (Position, Position)) extends PStmt
 
@@ -1465,16 +1540,37 @@ case class PAssume(assume: PKw.Assume, e: PExp)(val pos: (Position, Position)) e
 case class PInhale(inhale: PKw.Inhale, e: PExp)(val pos: (Position, Position)) extends PStmt
 
 /** Can also represent a method call or statement macro with no `:=` when `targets` is empty. */
-case class PAssign(targets: PDelimited[PExp with PAssignTarget, PSym.Comma], op: Option[PSymOp.Assign], rhs: PExp)(val pos: (Position, Position)) extends PStmt
+case class PAssign(targets: PDelimited[PExp with PAssignTarget, PSym.Comma], op: Option[PSymOp.Assign], rhs: PExp)(val pos: (Position, Position)) extends PStmt {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    if (targets.isEmpty) {
+      show(rhs)
+    } else {
+      show(targets) <> showOption(op) <> rne(show(rhs))
+    }
+  }
+}
 
 sealed trait PIfContinuation extends PStmt
-case class PIf(keyword: PReserved[PKeywordIf], cond: PGrouped.Paren[PExp], thn: PSeqn, els: Option[PIfContinuation])(val pos: (Position, Position)) extends PStmt with PIfContinuation
+case class PIf(keyword: PReserved[PKeywordIf], cond: PGrouped.Paren[PExp], thn: PSeqn, els: Option[PIfContinuation])(val pos: (Position, Position)) extends PStmt with PIfContinuation {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = show(keyword) <> show(cond) <>
+    showBody(thn, false) <> els.map(showBody(_, false)).getOrElse(rn())
+
+}
 case class PElse(k: PKw.Else, els: PSeqn)(val pos: (Position, Position)) extends PStmt with PIfContinuation
 
-case class PWhile(keyword: PKw.While, cond: PGrouped.Paren[PExp], invs: PDelimited[PSpecification[PKw.InvSpec], Option[PSym.Semi]], body: PSeqn)(val pos: (Position, Position)) extends PStmt
+case class PWhile(keyword: PKw.While, cond: PGrouped.Paren[PExp], invs: PDelimited[PSpecification[PKw.InvSpec], Option[PSym.Semi]], body: PSeqn)(val pos: (Position, Position)) extends PStmt {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    show(keyword) <> show(cond) <+>
+      showInvs(invs) <> showBody(body, !invs.isEmpty)
+  }
+}
 
 case class PVars(keyword: PKw.Var, vars: PDelimited[PLocalVarDecl, PSym.Comma], init: Option[(PSymOp.Assign, PExp)])(val pos: (Position, Position)) extends PStmt {
   def assign: Option[PAssign] = init map (i => PAssign(vars.update(vars.toSeq.map(_.toIdnUse)), Some(i._1), i._2)(pos))
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] =
+    show(keyword) <> show(vars) <>
+      init.map(s => rne(rg(show(s._1) <@> show(s._2)))).getOrElse(rn())
 }
 
 case class PLabel(label: PKw.Label, idndef: PIdnDef, invs: PDelimited[PSpecification[PKw.InvSpec], Option[PSym.Semi]])(val pos: (Position, Position)) extends PStmt with PMemberDeclaration with PBackwardDeclaration
@@ -1617,7 +1713,12 @@ trait PNoSpecsFunction extends PAnyFunction {
 ///////////////////////////////////////////////////////////////////////////
 // Program Members
 
-case class PProgram(imported: Seq[PProgram], members: Seq[PMember])(val pos: (Position, Position), val localErrors: Seq[ParseReport]) extends PNode {
+case class PProgram(imported: Seq[PProgram], members: Seq[PMember])(
+  val pos: (Position, Position),
+  val localErrors: Seq[ParseReport],
+  var offsets: Seq[Int],
+  var rawProgram: String
+) extends PNode {
   val imports: Seq[PImport] = members.collect { case i: PImport => i } ++ imported.flatMap(_.imports)
   val macros: Seq[PDefine] = members.collect { case m: PDefine => m } ++ imported.flatMap(_.macros)
   val domains: Seq[PDomain] = members.collect { case d: PDomain => d } ++ imported.flatMap(_.domains)
@@ -1634,20 +1735,28 @@ case class PProgram(imported: Seq[PProgram], members: Seq[PMember])(val pos: (Po
     val i = imported.map(_.pretty).mkString("\n")
     prefix + m + "\n\n" + i
   }
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    if (members.isEmpty)
+      rn()
+    else
+      members.zipWithIndex.map(e => (if (e._2 == 0) rn() else rlb()) <> show(e._1)).reduce((acc, n) => acc <> n)
+  }
+
   // Pretty print members in a specific order
   def prettyOrdered: String = {
     val all = Seq(imports, macros, domains, fields, functions, predicates, methods, extensions).filter(_.length > 0)
     all.map(_.map(_.pretty).mkString("\n")).mkString("\n")
   }
 
-  override def getExtraVals: Seq[Any] = Seq(pos, localErrors)
+  override def getExtraVals: Seq[Any] = Seq(pos, localErrors, offsets, rawProgram)
 
-  def filterMembers(f: PMember => Boolean): PProgram = PProgram(imported.map(_.filterMembers(f)), members.filter(f))(pos, localErrors)
-  def newImported(newImported: Seq[PProgram]): PProgram = if (newImported.isEmpty) this else PProgram(imported ++ newImported, members)(pos, localErrors)
+  def filterMembers(f: PMember => Boolean): PProgram = PProgram(imported.map(_.filterMembers(f)), members.filter(f))(pos, localErrors, offsets, rawProgram)
+  def newImported(newImported: Seq[PProgram]): PProgram = if (newImported.isEmpty) this else PProgram(imported ++ newImported, members)(pos, localErrors, offsets, rawProgram)
 }
 
 object PProgram {
-  def error(error: ParseReport): PProgram = PProgram(Nil, Nil)((error.pos, error.pos), Seq(error))
+  def error(error: ParseReport): PProgram = PProgram(Nil, Nil)((error.pos, error.pos), Seq(error), Nil, "")
 }
 
 case class PImport(annotations: Seq[PAnnotation], imprt: PKw.Import, file: PStringLiteral)(val pos: (FilePosition, FilePosition)) extends PMember with PPrettySubnodes {
@@ -1658,11 +1767,22 @@ case class PImport(annotations: Seq[PAnnotation], imprt: PKw.Import, file: PStri
 
 case class PDefineParam(idndef: PIdnDef)(val pos: (Position, Position)) extends PNode with PLocalDeclaration with PPrettySubnodes
 
-case class PDefine(annotations: Seq[PAnnotation], define: PKw.Define, idndef: PIdnDef, parameters: Option[PDelimited.Comma[PSym.Paren, PDefineParam]], body: PNode)(val pos: (FilePosition, FilePosition)) extends PSingleMember with PStmt with PNameAnalyserOpaque
+case class PDefine(annotations: Seq[PAnnotation], define: PKw.Define, idndef: PIdnDef, parameters: Option[PDelimited.Comma[PSym.Paren, PDefineParam]], body: PNode)(val pos: (FilePosition, FilePosition)) extends PSingleMember with PStmt with PNameAnalyserOpaque {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    showAnnotations(annotations) <> show(define) <> show(idndef) <> showOption(parameters) <+> show(body)
+  }
+}
 
 case class PDomain(annotations: Seq[PAnnotation], domain: PKw.Domain, idndef: PIdnDef, typVars: Option[PDelimited.Comma[PSym.Bracket, PTypeVarDecl]], interpretations: Option[PDomainInterpretations], members: PGrouped[PSym.Brace, PDomainMembers])
                   (val pos: (Position, Position)) extends PSingleMember with PTypeDeclaration with PPrettySubnodes {
   def typVarsSeq: Seq[PTypeVarDecl] = typVars.map(_.inner.toSeq).getOrElse(Nil)
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    showAnnotations(annotations) <> show(domain) <>
+      show(idndef) <> showOption(typVars) <>
+      (if (interpretations.isEmpty) rn() else rne(rlb() <> showOption(interpretations))) <>
+      showBody(members, !interpretations.isEmpty)
+  }
 }
 
 case class PDomainFunctionInterpretation(k: PKw.Interpretation, i: PStringLiteral)(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
@@ -1675,13 +1795,20 @@ case class PDomainFunction(annotations: Seq[PAnnotation], unique: Option[PKw.Uni
   override def body = None
 }
 
-case class PAxiom(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp)(val pos: (Position, Position)) extends PDomainMember with PPrettySubnodes
-case class PDomainMembers(funcs: PDelimited[PDomainFunction, Option[PSym.Semi]], axioms: PDelimited[PAxiom, Option[PSym.Semi]])(val pos: (Position, Position)) extends PNode {
+case class PAxiom(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp)(val pos: (Position, Position)) extends PDomainMember with PPrettySubnodes {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = showAnnotations(annotations) <> show(axiom) <>
+    showOption(idndef) <+> show(exp)
+}
+case class PDomainMembers(funcs: PDelimited[PDomainFunction, Option[PSym.Semi]], axioms: PDelimited[PAxiom, Option[PSym.Semi]])(val pos: (Position, Position), val original: PDomainMembers1) extends PNode {
   override def pretty: String = {
     val fPretty = if (funcs.length == 0) "" else s"\n  ${funcs.prettyLines.replace("\n", "\n  ")}\n"
     val aPretty = if (axioms.length == 0) "" else s"\n  ${axioms.prettyLines.replace("\n", "\n  ")}\n"
     s"${fPretty}${aPretty}"
   }
+
+  override def getExtraVals: Seq[Any] = Seq(pos, original)
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = show(original)
 }
 
 case class PDomainInterpretation(name: PRawString, c: PSym.Colon, lit: PStringLiteral)(val pos: (Position, Position)) extends PNode with PPrettySubnodes
@@ -1691,8 +1818,15 @@ case class PDomainInterpretations(k: PReserved[PKeywordLang], m: PDelimited.Comm
 
 trait PDomainMember1 extends PNode with PPrettySubnodes
 case class PDomainFunction1(annotations: Seq[PAnnotation], unique: Option[PKw.Unique], function: PKw.FunctionD, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PDomainFunctionArg], c: PSym.Colon, typ: PType, interpretation: Option[PDomainFunctionInterpretation], s: Option[PSym.Semi])(val pos: (Position, Position)) extends PDomainMember1
-case class PAxiom1(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp, s: Option[PSym.Semi])(val pos: (Position, Position)) extends PDomainMember1
-case class PDomainMembers1(members: Seq[PDomainMember1])(val pos: (Position, Position)) extends PNode with PPrettySubnodes
+case class PAxiom1(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp, s: Option[PSym.Semi])(val pos: (Position, Position)) extends PDomainMember1 {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = showAnnotations(annotations) <> show(axiom) <>
+    showOption(idndef) <+> show(exp) <> showOption(s)
+}
+case class PDomainMembers1(members: Seq[PDomainMember1])(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = if (members.isEmpty) rn() else members.zipWithIndex
+    .map(m => if (m._2 == 0) show(m._1) else rlb() <> show(m._1))
+    .reduce(_ <> _)
+}
 
 
 case class PFields(annotations: Seq[PAnnotation], field: PKw.Field, fields: PDelimited[PFieldDecl, PSym.Comma], s: Option[PSym.Semi])(val pos: (Position, Position)) extends PMember with PPrettySubnodes {
@@ -1704,18 +1838,32 @@ case class PSpecification[+T <: PKw.Spec](k: PReserved[PKw.Spec], e: PExp)(val p
 }
 
 case class PFunction(annotations: Seq[PAnnotation], keyword: PKw.Function, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl], c: PSym.Colon, resultType: PType, pres: PDelimited[PSpecification[PKw.PreSpec], Option[PSym.Semi]], posts: PDelimited[PSpecification[PKw.PostSpec], Option[PSym.Semi]], body: Option[PBracedExp])
-                    (val pos: (Position, Position)) extends PSingleMember with PAnyFunction with PGlobalCallableNamedArgs with PPrettySubnodes
+                    (val pos: (Position, Position)) extends PSingleMember with PAnyFunction with PGlobalCallableNamedArgs with PPrettySubnodes {
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    showAnnotations(annotations) <> show(keyword) <> show(idndef) <>
+      show(args) <> show(c) <> show(resultType) <>
+      showPresPosts(pres, posts) <> body.map(showBody(_, !(pres.isEmpty && posts.isEmpty))).getOrElse(rn())
+  }
+}
 
 case class PPredicate(annotations: Seq[PAnnotation], keyword: PKw.Predicate, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl], body: Option[PBracedExp])(val pos: (Position, Position))
   extends PSingleMember with PNoSpecsFunction with PGlobalCallableNamedArgs with PPrettySubnodes {
   override def c = PReserved.implied(PSym.Colon)
   override def resultType = Predicate
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] =  showAnnotations(annotations) <> show(keyword) <> show(idndef) <>
+    show(args) <> body.map(showBody(_, false)).getOrElse(rn())
 }
 
 case class PMethod(annotations: Seq[PAnnotation], keyword: PKw.Method, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl], returns: Option[PMethodReturns], pres: PDelimited[PSpecification[PKw.PreSpec], Option[PSym.Semi]], posts: PDelimited[PSpecification[PKw.PostSpec], Option[PSym.Semi]], body: Option[PSeqn])
                   (val pos: (Position, Position)) extends PSingleMember with PGlobalCallableNamedArgs with PPrettySubnodes {
   def formalReturns: Seq[PFormalReturnDecl] = returns.map(_.formalReturns.inner.toSeq).getOrElse(Nil)
   override def returnNodes = returns.toSeq
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    showAnnotations(annotations) <> show(keyword) <> show(idndef) <> show(args) <> showReturns(returns) <>
+      showPresPosts(pres, posts) <> body.map(showBody(_, !(returns.isEmpty && pres.isEmpty && posts.isEmpty))).getOrElse(rn())
+  }
 }
 
 case class PMethodReturns(k: PKw.Returns, formalReturns: PGrouped.Paren[PDelimited[PFormalReturnDecl, PSym.Comma]])(val pos: (Position, Position)) extends PNode with PPrettySubnodes
@@ -1727,6 +1875,7 @@ case class PAnnotationsPosition(annotations: Seq[PAnnotation], pos: (FilePositio
 
 case class PAnnotation(at: PSym.At, key: PRawString, values: PGrouped.Paren[PDelimited[PStringLiteral, PSym.Comma]])(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
   override def pretty: String = super.pretty + "\n"
+  override def rightPad: RNode = RLineBreak()
 }
 
 // Any unenclosed string (e.g. `hello`)
@@ -1753,4 +1902,24 @@ trait PExtender extends PNode {
   def translateExp(t: Translator): Exp = ???
 
   def translateType(t: Translator): Type = ???
+}
+
+// Trivia (comments, whitespaces)
+trait PTrivia
+case class PSpace() extends PTrivia
+case class PNewLine() extends PTrivia
+
+case class PComment(inner: String, trimmed: Boolean) extends PTrivia {
+  def str: String = inner
+}
+
+object PComment {
+  def apply(inner: String): PComment = {
+    // For line comments, the parser will by default include the newline
+    // in the comment. However, for the reformatter it is important that
+    // we strip the newline from the comment and add it manually via a
+    // linebreak instead, so we strip it here.
+    val trimmed = inner.endsWith("\n") || inner.endsWith("\r\n");
+    PComment(inner.trim, trimmed)
+  }
 }
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
index daed9a67f..6db72e749 100644
--- a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
+++ b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
@@ -7,18 +7,31 @@
 package viper.silver.parser
 
 import viper.silver.ast.{NoPosition, Position}
+import viper.silver.parser.PSym.Brace
+import viper.silver.parser.RNode._
+import viper.silver.parser.ReformatPrettyPrinter.{show, showAny}
 import viper.silver.parser.TypeHelper._
 
 trait PReservedString {
   def token: String
   def display: String = s"$leftPad$token$rightPad"
-  def leftPad: String = ""
-  def rightPad: String = ""
+  def leftPad: Boolean = false
+  def rightPad: Boolean = false
+  
+  // Unfortunately, there are a few cases where leftPad/rightPad (which are used for the
+  // pretty-printer) are not the same as required for the reformatter, so we need
+  // to keep them as separate variables and override them in certain cases.
+  def reformatLeftPad: RNode = if (leftPad) { RSpace() } else { RNil() }
+  def reformatRightPad: RNode = if (rightPad) { RSpace() } else { RNil() }
 }
-trait LeftSpace extends PReservedString { override def leftPad = " " }
-trait RightSpace extends PReservedString { override def rightPad = " " }
+trait LeftSpace extends PReservedString { override def leftPad = true }
+trait RightSpace extends PReservedString { override def rightPad = true }
 case class PReserved[+T <: PReservedString](rs: T)(val pos: (Position, Position)) extends PNode with PLeaf {
   override def display = rs.display
+
+  override def leftPad: RNode = rs.reformatLeftPad
+  override def rightPad: RNode = rs.reformatRightPad
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = rt(rs.token)
 }
 object PReserved {
   def implied[T <: PReservedString](rs: T): PReserved[T] = PReserved(rs)(NoPosition, NoPosition)
@@ -31,6 +44,21 @@ case class PGrouped[G <: PSym.Group, +T](l: PReserved[G#L], inner: T, r: PReserv
     val iPretty = if (inner.length == 0) "" else s"\n  ${inner.prettyLines.replace("\n", "\n  ")}\n"
     s"${l.pretty}${iPretty}${r.pretty}"
   }
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    if (l.rs.isInstanceOf[Brace]) {
+      val left = show(l);
+      val inner_ = showAny(inner);
+      val right = show(r);
+      if (inner_.forall(_.isNil)) {
+        left <> right
+      } else {
+        left <> rne(rl() <> inner_) <> rl() <> right
+      }
+    } else  {
+      show(l) <> rne(showAny(inner)) <> show(r)
+    }
+  }
 }
 object PGrouped {
   /** Grouped and delimited. */
@@ -83,6 +111,24 @@ class PDelimited[+T, +D](
   }
   override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(first, inner, end)
   override def toString(): String = s"PDelimited($first,$inner,$end)"
+
+  override def reformat(implicit ctx: ReformatterContext): List[RNode] = {
+    if (isEmpty) {
+      return rn()
+    }
+
+    val separator = delimiters.headOption match {
+      // Commas will already add a space for padding by default,
+      // so we don't add anything here.
+      case Some(_: PSym.Comma) => rn()
+      case None => rn()
+      case _ => rlb()
+    }
+
+    showAny(first) <>
+      inner.foldLeft(rn())((acc, b) => acc <> showAny(b._1) <> separator <> showAny(b._2)) <>
+      showAny(end)
+  }
 }
 
 object PDelimited {
@@ -147,7 +193,9 @@ object PKw {
   type Predicate = PReserved[Predicate.type]
   case object Domain extends PKw("domain") with PKeywordLang
   type Domain = PReserved[Domain.type]
-  case object Interpretation extends PKw("interpretation") with PKeywordLang
+  case object Interpretation extends PKw("interpretation") with PKeywordLang {
+    override def reformatLeftPad: RNode = RSpace()
+  }
   type Interpretation = PReserved[Interpretation.type]
   case object Axiom extends PKw("axiom") with PKeywordLang
   type Axiom = PReserved[Axiom.type]
@@ -167,7 +215,7 @@ object PKw {
   type Invariant = PReserved[Invariant.type]
 
   case object Result extends PKw("result") with PKeywordLang with PKeywordAtom {
-    override def rightPad = ""
+    override def rightPad = false
   }
   type Result = PReserved[Result.type]
   case object Exists extends PKw("exists") with PKeywordLang with PKeywordAtom
@@ -177,12 +225,12 @@ object PKw {
   case object Forperm extends PKw("forperm") with PKeywordLang with PKeywordAtom
   type Forperm = PReserved[Forperm.type]
   case object New extends PKw("new") with PKeywordLang with PKeywordAtom {
-    override def rightPad = ""
+    override def rightPad = false
   }
   type New = PReserved[New.type]
 
   case object Lhs extends PKw("lhs") with PKeywordLang {
-    override def rightPad = ""
+    override def rightPad = false
   }
   type Lhs = PReserved[Lhs.type]
 
@@ -342,7 +390,10 @@ trait PSignaturesOp extends POperator {
   def signatures: List[PTypeSubstitution]
 }
 trait PUnaryOp extends POperator with PSignaturesOp
-trait PBinaryOp extends POperator with PSignaturesOp with LeftSpace with RightSpace
+trait PBinaryOp extends POperator with PSignaturesOp with LeftSpace with RightSpace {
+  override def reformatLeftPad: RNode = RNil()
+  override def reformatRightPad: RNode = RNil()
+}
 trait PArithOp extends PBinaryOp {
   override def signatures = List(
     Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int),
@@ -441,7 +492,7 @@ object PSymOp {
   type Dot = PReserved[Dot.type]
   case object DotDot  extends PSym("..")  with PSymbolOp
   type DotDot = PReserved[DotDot.type]
-  case object Comma   extends PSym(",")   with PSymbolOp
+  case object Comma   extends PSym(",")   with PSymbolOp with RightSpace
   type Comma = PReserved[Comma.type]
   case object RParen  extends PSym(")")   with PSymbolOp
   type RParen = PReserved[RParen.type]
diff --git a/src/main/scala/viper/silver/parser/ReformatPrettyPrinter.scala b/src/main/scala/viper/silver/parser/ReformatPrettyPrinter.scala
new file mode 100644
index 000000000..f96a40e5a
--- /dev/null
+++ b/src/main/scala/viper/silver/parser/ReformatPrettyPrinter.scala
@@ -0,0 +1,445 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2024 ETH Zurich.
+
+/**
+ * The idea behind how the reformatter works is as follows:
+ *
+ * Firstly, it's based on the parse AST (PProgram) and not the Viper AST (Program), which actually already has
+ * a pretty printing functionality. But it's not suitable for actual reformatting for a couple of reasons:
+ * At the point where we generate the AST, it's already processed in a way that makes it unsuitable for formatting.
+ * For examples, macros will be expanded, imports will be inlined, and most importantly, information about whitespaces
+ * and comments is completely discarded, and so on. Because of this, using the parse AST as a basis for the formatter
+ * is just more sensible.
+ *
+ * The steps are as follows:
+ * - We first build the parse AST for a specific Viper file.
+ * - Then, we iterate over each node in the tree and turn it into a list of RNodes. A RNode is very similar
+ *   to the primitives provided by `PrettyPrintPrimitives`, the reason we don't convert directly into a pretty
+ *   print tree is that we need to perform some preprocessing on whitespaces, which is just much easier to do
+ *   if we store everything in an intermediate representation.
+ * - Whenever we hit a leaf node, we get all comments and whitespaces that appear from the last position
+ *   we stored up to that leaf node, and print them. This is necessary to preserve comments and certain kinds of
+ *   newlines, which is important when reformatting a file.
+ * - Once we have our finalized list of RNodes, we convert them into a pretty print tree and print that tree,
+ *   similarly to how it's done for the pretty printer for the Viper AST.
+ */
+
+package viper.silver.parser
+
+import fastparse.Parsed
+import viper.silver.ast
+import viper.silver.ast.HasLineColumn
+import viper.silver.ast.pretty.FastPrettyPrinterBase
+import viper.silver.parser.FastParserCompanion.pTrivia
+import viper.silver.parser.RNode._
+
+import scala.collection.mutable.ArrayBuffer
+
+// A reformattable node.
+trait RNode {
+  def isNil: Boolean
+}
+trait RCommentFragment
+trait RWhitespace extends RNode with RCommentFragment
+
+object RNode {
+  def rn(): List[RNode] = List(RNil())
+  def rne(l: List[RNode]): List[RNode] = List(RNest(l))
+  def rg(l: List[RNode]): List[RNode] = List(RGroup(l))
+  def rt(text: String): List[RNode] = List(RText(text))
+  def rs(): List[RNode] = List(RSpace())
+  def rl(): List[RNode] = List(RLine())
+  def rlb(): List[RNode] = List(RLineBreak())
+}
+
+case class RNil() extends RNode {
+  override def isNil: Boolean = true
+}
+
+case class RText(text: String) extends RNode {
+  override def isNil: Boolean = text.isEmpty
+}
+
+case class RTrivia(l: List[RCommentFragment]) extends RNode {
+  override def isNil: Boolean = l.isEmpty
+
+  def hasComment(): Boolean = l.exists(_ match {
+    case RComment(_) => true
+    case _ => false
+  })
+
+  def trimmedLw(): RTrivia = l.headOption match {
+    case Some(_: RWhitespace) => RTrivia(l.tail)
+    case _ => this
+  }
+
+  def replacedLw(r: RWhitespace): RTrivia = l.headOption match {
+    case Some(_: RWhitespace) => RTrivia(r :: l.tail)
+    case _ => this
+  }
+}
+
+case class RComment(comment: PComment) extends RCommentFragment
+
+case class RNest(l: List[RNode]) extends RNode {
+  override def isNil: Boolean = l.forall(_.isNil)
+}
+
+case class RGroup(l: List[RNode]) extends RNode {
+  override def isNil: Boolean = l.forall(_.isNil)
+}
+
+case class RSpace() extends RWhitespace with RCommentFragment {
+  override def isNil: Boolean = false
+}
+
+case class RLine() extends RWhitespace {
+  override def isNil: Boolean = false
+}
+
+case class RLineBreak() extends RWhitespace with RCommentFragment {
+  override def isNil: Boolean = false
+}
+
+case class RDLineBreak() extends RWhitespace with RCommentFragment {
+  override def isNil: Boolean = false
+}
+
+sealed trait ReformatPrettyPrinterBase extends FastPrettyPrinterBase {
+  override val defaultIndent = 4
+  override val defaultWidth = 75
+}
+
+trait ReformatBase {
+  implicit class ContOps(dl: List[RNode]) {
+    def com(dr: List[RNode]): List[RNode] =
+      dl ::: dr
+
+    def <>(dr: List[RNode]): List[RNode] =
+      if (dl.forall(_.isNil)) dr else if (dr.forall(_.isNil)) dl else dl com dr
+
+    def <+>(dr: List[RNode]): List[RNode] =
+      if (dr.forall(_.isNil)) dl else if (dl.forall(_.isNil)) dr else dl ::: rs() ::: dr
+
+    def <@>(dr: List[RNode]): List[RNode] =
+      if (dr.forall(_.isNil)) dl else if (dl.forall(_.isNil)) dr else dl ::: rl() ::: dr
+  }
+}
+
+trait Reformattable extends ReformatBase with Where {
+  def reformat(implicit ctx: ReformatterContext): List[RNode]
+  def rightPad: RNode = RNil()
+  def leftPad: RNode = RNil()
+}
+
+trait ReformattableExpression extends ReformatBase with PNode {
+  def reformatExp(implicit ctx: ReformatterContext): List[RNode] = this match {
+    case p: PLeaf => rt(p.pretty)
+    case _ => ReformatPrettyPrinter.reformatNodesNoSpace(this)
+  }
+}
+
+class ReformatterContext(val program: String, val offsets: Seq[Int]) {
+  // Store the last position we have processed, so we don't include certain trivia
+  // twice.
+  var currentOffset: Int = 0
+
+  def getByteOffset(p: HasLineColumn): Int = {
+    val row = offsets(p.line - 1);
+    row + p.column - 1
+  }
+
+  // Get all trivia for a node position. The first position
+  // is the start position of the node (i.e. the end position when getting
+  // the trivia) and the second position is the end position of the node (i.e.
+  // the value `currentOffset` should be updated to).
+  def getTrivia(pos: (ast.Position, ast.Position)): RTrivia = {
+    (pos._1, pos._2) match {
+      case (p: HasLineColumn, q: HasLineColumn) => {
+        val p_offset = getByteOffset(p);
+        val q_offset = getByteOffset(q);
+        getTriviaByByteOffset(p_offset, q_offset)
+      }
+      case _ => RTrivia(List())
+    }
+  }
+
+  def getTriviaByByteOffset(end: Int, updateOffset: Int): RTrivia = {
+    if (currentOffset <= end) {
+      val str = program.substring(currentOffset, end);
+      currentOffset = updateOffset
+
+      fastparse.parse(str, pTrivia(_)) match {
+        case Parsed.Success(value, _) => {
+          // Create a list of deduplicated whitespaces, and comments.
+          val trivia = ArrayBuffer[RCommentFragment]()
+          var newlines = 0
+          var spaces = 0
+
+          val addTrivia = () => if (newlines > 1) {
+            trivia += RDLineBreak()
+          } else if (newlines > 0) {
+            trivia += RLineBreak()
+          } else if (spaces > 0) {
+            trivia += RSpace()
+          }
+
+          for (t <- value) {
+            t match {
+              case p: PComment => {
+                addTrivia()
+                trivia += RComment(p)
+
+                newlines = 0
+                spaces = 0
+
+                // In case we had a line comment, add the linebreak
+                // manually, since it was stripped in PComment.
+                if (p.trimmed) {
+                  newlines += 1
+                }
+              }
+              case _: PNewLine => newlines += 1
+              case _: PSpace => spaces += 1
+              case _ =>
+            }
+          }
+
+          addTrivia()
+
+          RTrivia(trivia.toList)
+        }
+        case _: Parsed.Failure => RTrivia(List())
+      }
+    } else {
+      RTrivia(List())
+    };
+  }
+}
+
+class PrettyPrintContext {
+  var whitespace: Option[RWhitespace] = None
+
+  def register(w: RWhitespace): Unit = {
+    whitespace match {
+      case None => whitespace = Some(w)
+      // If we already have a linebreak, it should not be overwritten e.g. by a space,
+      // and special handling applies in case we want a double line break.
+      case Some(_: RLineBreak) => w match {
+        case _: RLineBreak => whitespace = Some(RDLineBreak())
+        case _: RDLineBreak => whitespace = Some(RDLineBreak())
+        case _ =>
+      }
+      case Some(_) => whitespace = Some(w)
+    }
+  }
+}
+
+object ReformatPrettyPrinter extends ReformatPrettyPrinterBase with ReformatBase {
+  def hasLeadingLwNode(l: List[RNode]): Boolean = l.headOption.map(_ match {
+    case p: RGroup => hasLeadingLwNode(p.l)
+    case p: RNest => hasLeadingLwNode(p.l)
+    case _: RWhitespace => true
+    case _ => false
+  }).getOrElse(false)
+  
+  def reformatProgram(p: PProgram): String = {
+    implicit val ctx = new ReformatterContext(p.rawProgram, p.offsets)
+
+    def showWhitespace(w: RWhitespace): Cont = {
+      w match {
+        case RSpace() => space
+        case RLine() => line
+        case RLineBreak() => linebreak
+        case RDLineBreak() => linebreak <> linebreak
+      }
+    }
+    
+    def flushWhitespace(pc: PrettyPrintContext): Cont = {
+      val cont = pc.whitespace.map(showWhitespace(_)).getOrElse(nil)
+      pc.whitespace = None
+      
+      cont
+    }
+
+    def showTrivia(p: RTrivia): Cont = {
+      if (p.l.isEmpty) {
+        nil
+      } else {
+        p.l.map(t => t match {
+          case w: RWhitespace => showWhitespace(w)
+          case p: RComment => text(p.comment.str)
+        }).reduce((acc, n) => acc <> n)
+      };
+    }
+
+    def showNode(p: RNode, pc: PrettyPrintContext): Cont = {
+      p match {
+        case RNil() => nil
+        case w: RWhitespace => {
+          pc.register(w)
+
+          nil
+        }
+        case RText(t: String) => {
+          flushWhitespace(pc) <> text(t)
+        }
+        case t: RTrivia => {
+          val trivia = if (t.hasComment()) {
+            // If we already had a whitespace as part of formatting the program, we might have to
+            // trim the leading whitespace from the trivia.
+            pc.whitespace match {
+              case None => showTrivia(t)
+              // If we want a double linebreak and we already had a linebreak, replace it with a simple linebreak.
+              case Some(_: RLineBreak) => if (t.l.headOption == Some(RDLineBreak())) {
+                 showTrivia(t.replacedLw(RLineBreak()))
+                } else {
+                 showTrivia(t.trimmedLw())
+              }
+              // If we want a space and already had a space, do not write double space, trim it instead.
+              case Some(_: RSpace) => if (t.l.headOption == Some(RSpace())) {
+                showTrivia(t.trimmedLw())
+              } else {
+                showTrivia(t)
+              }
+              case Some(_) => showTrivia(t.trimmedLw())
+            }
+          } else {
+            val newlines = t.l.map(_ match {
+              case RLineBreak() => 1
+              case RDLineBreak() => 2
+              case _ => 0
+            }).sum
+
+            pc.whitespace match {
+              case Some(_: RLineBreak) => if (newlines > 1) linebreak else nil
+              case _ => nil
+            }
+          }
+          
+          flushWhitespace(pc) <> trivia
+        }
+        case RGroup(l: List[RNode]) => {
+          val lw = flushWhitespace(pc) 
+          val grouped = group(showList(l, pc))
+          
+          if (hasLeadingLwNode(l)) {
+            grouped
+          } else {
+            // Only add the leading whitespace if the current group doesn't start with one.
+            lw <> grouped
+          }
+        }
+        case RNest(l: List[RNode]) => {
+          val lw = flushWhitespace(pc)
+          val nested = nest(defaultIndent, showList(l, pc))
+          
+          if (hasLeadingLwNode(l)) {
+            nested
+          } else {
+            // Only add the leading whitespace if the current nesting doesn't start with one.
+            lw <> nested
+          }
+        }
+      }
+    }
+
+    def showList(p: List[RNode], pc: PrettyPrintContext): Cont = {
+      var reformatted = nil
+      for (n <- p) {
+        reformatted = reformatted <> showNode(n, pc)
+      }
+      reformatted
+    }
+
+    val pc = new PrettyPrintContext()
+    val mainProgram = show(p)
+    // Don't forget the trivia after the last program node, i.e. trailing comments!
+    val trailing = List(ctx.getTriviaByByteOffset(ctx.program.length, ctx.program.length))
+    val finalProgram = (mainProgram ::: trailing).filter(!_.isNil)      
+    super.pretty(defaultWidth, showList(finalProgram, pc))
+  }
+
+  def showOption[T <: Any](n: Option[T])(implicit ctx: ReformatterContext): List[RNode] = {
+    n match {
+      case Some(r) => showAny(r)
+      case None => rn()
+    }
+  }
+
+  def showAnnotations(annotations: Seq[PAnnotation])(implicit ctx: ReformatterContext): List[RNode] = {
+    if (annotations.isEmpty) {
+      List(RNil())
+    } else {
+      annotations.map(show(_)).reduce((acc, n) => acc <> n)
+    }
+  }
+
+  def showReturns(returns: Option[PMethodReturns])(implicit ctx: ReformatterContext): List[RNode] = {
+    returns.map(a => rs() ::: show(a)).getOrElse(rn())
+  }
+
+  def showPresPosts(pres: PDelimited[_, _], posts: PDelimited[_, _])(implicit ctx: ReformatterContext): List[RNode] = {
+    rne((if (pres.isEmpty) rn()
+    else rlb() ::: show(pres)) :::
+      (if (posts.isEmpty) rn()
+      else rlb() ::: show(posts)
+        )
+    )
+  }
+
+  def showInvs(invs: PDelimited[_, _])(implicit ctx: ReformatterContext): List[RNode] = {
+    rne(if (invs.isEmpty) rn() else rlb() ::: show(invs))
+  }
+
+  def showBody(body: Reformattable, newline: Boolean)(implicit ctx: ReformatterContext): List[RNode] = {
+    if (newline) {
+      rlb() ::: show(body)
+    } else {
+      rs() ::: show(body)
+    }
+  }
+
+  def show(r: Reformattable)(implicit ctx: ReformatterContext): List[RNode] = {
+    r match {
+      case _: PLeaf => {
+        List(r.leftPad) <> List(ctx.getTrivia(r.pos)) <> r.reformat(ctx) <> List(r.rightPad)
+      }
+      case _ => List(r.leftPad) <> r.reformat(ctx) <> List(r.rightPad)
+    }
+  }
+
+  // We need this method because unfortunately PGrouped and PDelimited can have arbitrary generic parameters.
+  def showAny(n: Any)(implicit ctx: ReformatterContext): List[RNode] = {
+    n match {
+      case p: Reformattable => show(p)
+      case p: Option[Any] => showOption(p)
+      case p: Seq[Any] => showSeq(p)
+      case p: Right[Any, Any] => showAny(p.value)
+      case p: Left[Any, Any] => showAny(p.value)
+      case p: Iterable[Any] => if (p.isEmpty) List() else p.map(showAny).reduce((a, b) => a <> b)
+      case p: Product =>
+        if (p.productArity == 0) List()
+        else (0 until p.productArity).map(i => showAny(p.productElement(i))).reduce((a, b) => a <> b)
+    }
+  }
+
+  def showSeq(l: Seq[Any])(implicit ctx: ReformatterContext): List[RNode] = {
+    if (l.isEmpty) {
+      rn()
+    } else {
+      l.zipWithIndex.map(e => if (e._2 == 0) showAny(e._1) else rlb() <> showAny(e._1)).reduce(_ <> _)
+    }
+  }
+  
+  def showNestedPaddedExpr(expr: PExp)(implicit ctx: ReformatterContext): List[RNode] = {
+    rne(rg(rl() <> show(expr)))
+  }
+
+  def reformatNodesNoSpace(n: PNode)(implicit ctx: ReformatterContext): List[RNode] = {
+    n.subnodes.map(show(_)).reduce(_ <> _)
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/plugin/ParserPluginTemplate.scala b/src/main/scala/viper/silver/plugin/ParserPluginTemplate.scala
index 71c0fc7cb..73a07e5d2 100644
--- a/src/main/scala/viper/silver/plugin/ParserPluginTemplate.scala
+++ b/src/main/scala/viper/silver/plugin/ParserPluginTemplate.scala
@@ -6,13 +6,12 @@
 
 package viper.silver.plugin
 
-import viper.silver.parser.{NameAnalyser, PAnnotationsPosition, PExp, PExtender, PKeyword, PSpecification, PKw, PMember, PReserved, PStmt, PTypeSubstitution, Translator, TypeChecker}
+import viper.silver.parser.{NameAnalyser, PAnnotationsPosition, PExp, PExtender, PKeyword, PKw, PMember, PReserved, PSpecification, PStmt, PTypeSubstitution, RNode, ReformatterContext, Translator, TypeChecker}
 import viper.silver.ast.pretty.PrettyPrintPrimitives
-import viper.silver.ast.{Declaration, ErrorTrafo, Exp, ExtensionExp, ExtensionMember, ExtensionStmt, Info, Member, Node, NoPosition, Position, Stmt, Type}
+import viper.silver.ast.{Declaration, ErrorTrafo, Exp, ExtensionExp, ExtensionMember, ExtensionStmt, Info, Member, NoPosition, Node, Position, Stmt, Type}
 import viper.silver.verifier.VerificationResult
 
 import scala.collection.Set
-
 import fastparse._
 
 trait ParserPluginTemplate {
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
index 4c9a0e870..729c5d53b 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
@@ -19,7 +19,9 @@ import viper.silver.ast.utility.rewriter.HasExtraVars
   */
 case object PAdtKeyword extends PKw("adt") with PKeywordLang
 case object PDerivesKeyword extends PKw("derives") with PKeywordLang
-case object PWithoutKeyword extends PKw("without") with PKeywordLang
+case object PWithoutKeyword extends PKw("without") with PKeywordLang {
+  override def reformatLeftPad: RNode = RSpace()
+}
 
 case class PAdt(annotations: Seq[PAnnotation], adt: PReserved[PAdtKeyword.type], idndef: PIdnDef, typVars: Option[PDelimited.Comma[PSym.Bracket, PTypeVarDecl]], c: PAdtSeq[PAdtConstructor], derive: Option[PAdtDeriving])
                (val pos: (Position, Position)) extends PExtender with PSingleMember with PGlobalDeclaration with PPrettySubnodes {
@@ -97,6 +99,9 @@ trait PAdtChild extends PNode {
 case class PAdtSeq[T <: PNode](seq: PGrouped[PSym.Brace, Seq[T]])(val pos: (Position, Position)) extends PExtender {
   def inner: Seq[T] = seq.inner
   override def pretty = s"${seq.l.pretty}\n  ${seq.inner.map(_.pretty).mkString("\n  ")}\n${seq.r.pretty}"
+
+  override def leftPad: RNode = RSpace()
+  override def rightPad: RNode = RSpace()
 }
 
 /** Any argument to a method, function or predicate. */
@@ -491,7 +496,7 @@ case class PDestructorCall(rcv: PExp, dot: PReserved[PDiscDot.type], idnref: PId
 }
 
 case object PIsKeyword extends PKwOp("is") {
-  override def rightPad = ""
+  override def rightPad = false
 }
 case object PDiscDot extends PSym(".") with PSymbolOp
 
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPASTExtension.scala
index 81ea1690b..5334bf269 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPASTExtension.scala
@@ -11,9 +11,13 @@ import viper.silver.parser.TypeHelper.Bool
 import viper.silver.parser._
 
 case object PDecreasesKeyword extends PKw("decreases") with PKeywordLang with PKw.AnySpec
-case object PIfKeyword extends PKw("if") with PKeywordLang
+case object PIfKeyword extends PKw("if") with PKeywordLang {
+  override def reformatLeftPad: RNode = RSpace()
+}
 
-case object PWildcardSym extends PSym("_") with PSymbolLang
+case object PWildcardSym extends PSym("_") with PSymbolLang {
+  override def reformatLeftPad: RNode = RSpace()
+}
 
 /**
  * Any possible decreases clause extends from this trait.
@@ -67,4 +71,3 @@ case class PDecreasesStar(star: PSym.Star)(val pos: (Position, Position)) extend
     DecreasesStar()(t.liftPos(this))
   }
 }
-
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index 50f8fe5c8..d1645cec2 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -194,7 +194,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       val importOnlyProgram = importStmts.mkString("\n")
       val importPProgram = PAstProvider.generateViperPAst(importOnlyProgram).get.filterMembers(_.isInstanceOf[PDomain])
       val inputFiltered = input.filterMembers(m => !(m.isInstanceOf[PDomain] && m.asInstanceOf[PDomain].idndef.name == "WellFoundedOrder"))
-      val mergedProgram = PProgram(inputFiltered.imported :+ importPProgram, inputFiltered.members)(input.pos, input.localErrors)
+      val mergedProgram = PProgram(inputFiltered.imported :+ importPProgram, inputFiltered.members)(input.pos, input.localErrors, input.offsets, input.rawProgram)
       super.beforeTranslate(mergedProgram)
     } else {
       super.beforeTranslate(input)
diff --git a/src/test/resources/reformatter/adts.vpr b/src/test/resources/reformatter/adts.vpr
new file mode 100644
index 000000000..37dbaeabf
--- /dev/null
+++ b/src/test/resources/reformatter/adts.vpr
@@ -0,0 +1,18 @@
+import <adt/derives.vpr>
+
+adt Tree[T, U, V] {
+    None1()
+    None2()
+}
+
+/**
+ * We define a list in a standard way, Nil() represents the empty list and Cons(x, xs)
+ * (from construct) represents a list with element x as its head and list xs as its tail.
+ * Note that while Viper supports generic ADTs, it does not support generic functions.
+ * So all functions operating on this ADT will be defined for a specific type, in this
+ * case Int.
+ */
+adt List2[T] {
+    Nil()
+    Cons(value: T,     tail: List2[T])
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/adts_expected.vpr b/src/test/resources/reformatter/adts_expected.vpr
new file mode 100644
index 000000000..d87ee0800
--- /dev/null
+++ b/src/test/resources/reformatter/adts_expected.vpr
@@ -0,0 +1,18 @@
+import <adt/derives.vpr>
+
+adt Tree[T, U, V] {
+    None1()
+    None2()
+}
+
+/**
+ * We define a list in a standard way, Nil() represents the empty list and Cons(x, xs)
+ * (from construct) represents a list with element x as its head and list xs as its tail.
+ * Note that while Viper supports generic ADTs, it does not support generic functions.
+ * So all functions operating on this ADT will be defined for a specific type, in this
+ * case Int.
+ */
+adt List2[T] {
+    Nil()
+    Cons(value: T, tail: List2[T])
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/annotations.vpr b/src/test/resources/reformatter/annotations.vpr
new file mode 100644
index 000000000..20837cae9
--- /dev/null
+++ b/src/test/resources/reformatter/annotations.vpr
@@ -0,0 +1,21 @@
+@annot()
+import <adt/derives.vpr>
+
+@annot1()
+function foo(): Int
+
+@annot1()function foo2(): Int
+
+@annot1()
+@annot2()@annot3()
+function foo3(): Int
+
+@annot1()
+domain Domain1[T] {
+    @annot1()@annot2()
+    axiom Axiom1 {
+        forall x: T :: true
+    }
+}
+
+@annot1()@annot2()predicate Pred1(t: Int)
\ No newline at end of file
diff --git a/src/test/resources/reformatter/annotations_expected.vpr b/src/test/resources/reformatter/annotations_expected.vpr
new file mode 100644
index 000000000..9001a2a83
--- /dev/null
+++ b/src/test/resources/reformatter/annotations_expected.vpr
@@ -0,0 +1,26 @@
+@annot()
+import <adt/derives.vpr>
+
+@annot1()
+function foo(): Int
+
+@annot1()
+function foo2(): Int
+
+@annot1()
+@annot2()
+@annot3()
+function foo3(): Int
+
+@annot1()
+domain Domain1[T] {
+    @annot1()
+    @annot2()
+    axiom Axiom1 {
+        forall x: T :: true
+    }
+}
+
+@annot1()
+@annot2()
+predicate Pred1(t: Int)
\ No newline at end of file
diff --git a/src/test/resources/reformatter/domains.vpr b/src/test/resources/reformatter/domains.vpr
new file mode 100644
index 000000000..7f5429618
--- /dev/null
+++ b/src/test/resources/reformatter/domains.vpr
@@ -0,0 +1,80 @@
+domain MyDomain[T, U] {
+    function foo(): Int
+    
+    function bar(x: Bool): Bool
+    
+    axiom axFoo {
+        foo() > 0
+    }
+    
+    axiom axBar {
+        bar(true)
+    }
+    
+    axiom axFoobar {
+        bar(false) ==> foo() == 3
+    }
+}
+domain MyDomain2interpretation
+    interpretation (hi: "bye", second: "third")
+{}
+
+domain MyDomain1 {
+    function foo4(): Int
+    
+    function bar4(x: Bool): Bool
+    
+    axiom axFoo1 {
+         foo4() > 0 }
+    
+    axiom axBar1 {
+        bar4(true)
+    }
+    
+    axiom axFoobar1 {
+        bar4(false) ==> foo4() == 3
+    }
+}
+
+domain MyType1[A, B] {
+    function constructor_a1(x: A): MyType1[A, B]
+    
+    function constructor_b1(y: B): MyType1[A, B]
+    
+    function bin_oper1(a: MyType1[A, B], b: MyType1[A, B]): MyType1[A, B]
+}
+
+domain MyInteger2 {
+    function create_int2(x: Int): MyInteger2
+    
+    function get_value2(a: MyInteger2): Int
+    
+    function sum3(a: MyInteger2, b: MyInteger2): MyInteger2
+    
+    axiom axSum {
+        forall a: MyInteger2, b: MyInteger2 ::{sum3(a, b)} sum3(a, b) == create_int2(get_value2(a) + get_value2(b))
+    }
+}
+
+domain IArray {
+    function slot(a: IArray, i: Int): Ref
+    function len(a: IArray): Int
+    function first4(r: Ref): IArray
+    function second4(r: Ref): Int
+    
+    axiom all_diff {
+        // A comment
+        forall a: IArray, i: Int   :: {
+                slot(a, i)
+            } first4(slot(a, i)) == a && second4(slot(a, i)) == i
+    }
+    
+    axiom len_nonneg {
+        forall a: IArray :: { len(a) } len(a) >= 0
+    }
+}
+
+domain myBV    interpretation (
+SMTLIB: "(_ BitVec 32)", Boogie: "bv32") {
+  function toBV32(i: Int): myBV interpretation      "(_ int2bv 32)"
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/domains_expected.vpr b/src/test/resources/reformatter/domains_expected.vpr
new file mode 100644
index 000000000..407c80255
--- /dev/null
+++ b/src/test/resources/reformatter/domains_expected.vpr
@@ -0,0 +1,86 @@
+domain MyDomain[T, U] {
+    function foo(): Int
+    
+    function bar(x: Bool): Bool
+    
+    axiom axFoo {
+        foo() > 0
+    }
+    
+    axiom axBar {
+        bar(true)
+    }
+    
+    axiom axFoobar {
+        bar(false) ==> foo() == 3
+    }
+}
+domain MyDomain2interpretation
+    interpretation (hi: "bye", second: "third")
+{}
+
+domain MyDomain1 {
+    function foo4(): Int
+    
+    function bar4(x: Bool): Bool
+    
+    axiom axFoo1 {
+        foo4() > 0
+    }
+    
+    axiom axBar1 {
+        bar4(true)
+    }
+    
+    axiom axFoobar1 {
+        bar4(false) ==> foo4() == 3
+    }
+}
+
+domain MyType1[A, B] {
+    function constructor_a1(x: A): MyType1[A, B]
+    
+    function constructor_b1(y: B): MyType1[A, B]
+    
+    function bin_oper1(a: MyType1[A, B], b: MyType1[A, B]): MyType1[A, B]
+}
+
+domain MyInteger2 {
+    function create_int2(x: Int): MyInteger2
+    
+    function get_value2(a: MyInteger2): Int
+    
+    function sum3(a: MyInteger2, b: MyInteger2): MyInteger2
+    
+    axiom axSum {
+        forall a: MyInteger2, b: MyInteger2 ::
+            {
+                sum3(a, b)
+            } sum3(a, b) == create_int2(get_value2(a) + get_value2(b))
+    }
+}
+
+domain IArray {
+    function slot(a: IArray, i: Int): Ref
+    function len(a: IArray): Int
+    function first4(r: Ref): IArray
+    function second4(r: Ref): Int
+    
+    axiom all_diff {
+        // A comment
+        forall a: IArray, i: Int ::
+            {
+                slot(a, i)
+            } first4(slot(a, i)) == a && second4(slot(a, i)) == i
+    }
+    
+    axiom len_nonneg {
+        forall a: IArray :: { len(a) } len(a) >= 0
+    }
+}
+
+domain myBV
+    interpretation (SMTLIB: "(_ BitVec 32)", Boogie: "bv32")
+{
+    function toBV32(i: Int): myBV interpretation "(_ int2bv 32)"
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/expressions.vpr b/src/test/resources/reformatter/expressions.vpr
new file mode 100644
index 000000000..c7f8d6047
--- /dev/null
+++ b/src/test/resources/reformatter/expressions.vpr
@@ -0,0 +1,20 @@
+method expressions(xs: List[Int]) {
+    var a_bool: Bool := true;
+    var a_very_long_boolean_name: Bool := true
+    var ter1: Int := xs.isNil ? 35343 : 34534;
+    var ter2: Int := xs.isNil ? 35343 + 345345345 + 34534534 + 345345435 : 34534;
+    var ter3: Int := (a_very_long_boolean_name && a_very_long_boolean_name && a_very_long_boolean_name) ? 35343 + 345345345 + 34534534 + 345345435 : 34534;
+    var ter4: Int := (a_very_long_boolean_name && a_very_long_boolean_name && a_very_long_boolean_name) ? 35343 + 345345345 + 34534534 + 345345435 : (34534 + 4353453 + 43534534);
+
+    var ter5: Int := xs.isNil ? 435453434 + 4546546456 + 34546456 : 3434534 + 34534543 + 3453453;
+    var ter6: Int := xs.isNil ? 435453434 + 4546546456 + 34546456 : 3434534 + 34534543 + 3453453 * 4534534 + 34534534 + 35645654 + 4353453543;
+    var ter7: Int := 23423434324 + 2342342342 + 344334534534 + 453453344534 + 3454354353345 + 45345345 + 435345345;
+    var ter8: Int :=
+        23423434324 - 2342342342 - 344334534534 - 453453344534 - 3454354353345 - 45345345 - 435345345;
+    var ter9: Int :=
+        23423434324 + 2342342342 + (344334534534 + 453453344534 + 3454354353345) + 45345345 + 435345345;
+
+    var bool_a: Bool := a_very_long_boolean_name && a_very_long_boolean_name
+    var bool_b: Bool := a_very_long_boolean_name && a_very_long_boolean_name || a_very_long_boolean_name && a_very_long_boolean_name;
+    var bool_c: Bool := a_very_long_boolean_name && a_very_long_boolean_name && (a_very_long_boolean_name || a_very_long_boolean_name) && a_very_long_boolean_name;
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/expressions_expected.vpr b/src/test/resources/reformatter/expressions_expected.vpr
new file mode 100644
index 000000000..a55e274da
--- /dev/null
+++ b/src/test/resources/reformatter/expressions_expected.vpr
@@ -0,0 +1,52 @@
+method expressions(xs: List[Int]) {
+    var a_bool: Bool := true;
+    var a_very_long_boolean_name: Bool := true
+    var ter1: Int := xs.isNil ? 35343 : 34534;
+    var ter2: Int :=
+        xs.isNil ? 35343 + 345345345 + 34534534 + 345345435 : 34534;
+    var ter3: Int :=
+        (a_very_long_boolean_name
+        && a_very_long_boolean_name && a_very_long_boolean_name) ?
+            35343 + 345345345 + 34534534 + 345345435 : 34534;
+    var ter4: Int :=
+        (a_very_long_boolean_name
+        && a_very_long_boolean_name && a_very_long_boolean_name) ?
+            35343 + 345345345 + 34534534 + 345345435 :
+            (34534 + 4353453 + 43534534);
+    
+    var ter5: Int :=
+        xs.isNil ?
+            435453434 + 4546546456 + 34546456 :
+            3434534 + 34534543 + 3453453;
+    var ter6: Int :=
+        xs.isNil ?
+            435453434 + 4546546456 + 34546456 :
+            3434534 + 34534543 + 3453453 * 4534534 + 34534534 + 35645654
+            + 4353453543;
+    var ter7: Int :=
+        23423434324 + 2342342342 + 344334534534 + 453453344534
+        + 3454354353345
+        + 45345345
+        + 435345345;
+    var ter8: Int :=
+        23423434324 - 2342342342 - 344334534534 - 453453344534
+        - 3454354353345
+        - 45345345
+        - 435345345;
+    var ter9: Int :=
+        23423434324 + 2342342342
+        + (344334534534 + 453453344534 + 3454354353345)
+        + 45345345
+        + 435345345;
+    
+    var bool_a: Bool :=
+        a_very_long_boolean_name && a_very_long_boolean_name
+    var bool_b: Bool :=
+        a_very_long_boolean_name && a_very_long_boolean_name
+        || a_very_long_boolean_name && a_very_long_boolean_name;
+    var bool_c: Bool :=
+        a_very_long_boolean_name
+        && a_very_long_boolean_name
+        && (a_very_long_boolean_name || a_very_long_boolean_name)
+        && a_very_long_boolean_name;
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/fields.vpr b/src/test/resources/reformatter/fields.vpr
new file mode 100644
index 000000000..df4d68045
--- /dev/null
+++ b/src/test/resources/reformatter/fields.vpr
@@ -0,0 +1,5 @@
+field val: Int
+field next: Ref;
+
+field left: Int
+field right: Int
\ No newline at end of file
diff --git a/src/test/resources/reformatter/fields_expected.vpr b/src/test/resources/reformatter/fields_expected.vpr
new file mode 100644
index 000000000..df4d68045
--- /dev/null
+++ b/src/test/resources/reformatter/fields_expected.vpr
@@ -0,0 +1,5 @@
+field val: Int
+field next: Ref;
+
+field left: Int
+field right: Int
\ No newline at end of file
diff --git a/src/test/resources/reformatter/functions.vpr b/src/test/resources/reformatter/functions.vpr
new file mode 100644
index 000000000..4879e33fa
--- /dev/null
+++ b/src/test/resources/reformatter/functions.vpr
@@ -0,0 +1,47 @@
+function gte(x: Ref, a: Int): Int
+    requires true
+    ensures true
+{
+    3
+}
+
+@annotation()
+function listLength(l: Ref): Int
+    requires list5(l)
+    ensures result > 0
+{
+    unfolding list5(l) in l.next5 == null ? 1 : 1 + listLength(l.next5)
+}
+
+/**
+ * A function in Viper represents a mathematical function and can be used
+ * in specifications and annotations, unlike methods. Because of that,
+ * functions must be deterministic and side-effect-free.
+ *
+ * This function computes the length of a list recursively.
+ */
+function length6(xs: List2[Int]): Int
+    /**
+     * Viper allows defining pre- and postconditions for functions. In this
+     * example, we only use postconditions, which are introduced with a 'ensures'
+     * keyword. The verifier will attempt to prove that the postcondition holds.
+     * To reference the return value of the function in a postcondition, we use the
+     * keyword 'result'.
+     */
+    ensures result >= 0  ensures xs.isNil ==> result == 0
+    ensures (xs.isCons ==> result == length6(xs.tail) + 1)
+    /**
+     * Unlike Dafny, Viper does not check for termination by default. To enable termination
+     * checking, we use a decreases clause. Here we have to specify the list parameter xs as
+     * the variable to prove termination upon. In each recursive call, the list gets one element
+     * shorter. For this proof to work, we need the well-founded order on lists imported above.
+     */
+    decreases xs
+{
+    /**
+     * Viper does not have a 'match' statement. All examples in Dafny that
+     * use this feature are translated to use destructors instead.
+     */
+    (xs.isNil) ? 
+    0 : (1 + length6(xs.tail))
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/functions_expected.vpr b/src/test/resources/reformatter/functions_expected.vpr
new file mode 100644
index 000000000..fb23ae0b5
--- /dev/null
+++ b/src/test/resources/reformatter/functions_expected.vpr
@@ -0,0 +1,47 @@
+function gte(x: Ref, a: Int): Int
+    requires true
+    ensures true
+{
+    3
+}
+
+@annotation()
+function listLength(l: Ref): Int
+    requires list5(l)
+    ensures result > 0
+{
+    unfolding list5(l) in l.next5 == null ? 1 : 1 + listLength(l.next5)
+}
+
+/**
+ * A function in Viper represents a mathematical function and can be used
+ * in specifications and annotations, unlike methods. Because of that,
+ * functions must be deterministic and side-effect-free.
+ *
+ * This function computes the length of a list recursively.
+ */
+function length6(xs: List2[Int]): Int
+    /**
+     * Viper allows defining pre- and postconditions for functions. In this
+     * example, we only use postconditions, which are introduced with a 'ensures'
+     * keyword. The verifier will attempt to prove that the postcondition holds.
+     * To reference the return value of the function in a postcondition, we use the
+     * keyword 'result'.
+     */
+    ensures result >= 0
+    ensures xs.isNil ==> result == 0
+    ensures (xs.isCons ==> result == length6(xs.tail) + 1)
+    /**
+     * Unlike Dafny, Viper does not check for termination by default. To enable termination
+     * checking, we use a decreases clause. Here we have to specify the list parameter xs as
+     * the variable to prove termination upon. In each recursive call, the list gets one element
+     * shorter. For this proof to work, we need the well-founded order on lists imported above.
+     */
+    decreases xs
+{
+    /**
+     * Viper does not have a 'match' statement. All examples in Dafny that
+     * use this feature are translated to use destructors instead.
+     */
+    (xs.isNil) ? 0 : (1 + length6(xs.tail))
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/macros.vpr b/src/test/resources/reformatter/macros.vpr
new file mode 100644
index 000000000..79d159c87
--- /dev/null
+++ b/src/test/resources/reformatter/macros.vpr
@@ -0,0 +1,18 @@
+define access5(a) forall j: Int ::
+    0 <= j && j < len(a) ==> acc(loc(a, j).val)
+    
+/**
+ * In the book, they use 'type PQueue = BraunTree'. This is not possible in 
+ * Viper. Therefore we will be using a macro to alias PQueue with BraunTree.
+ * This will allow us to follow the book more closely.
+ */
+define PQueue BraunTree
+
+
+
+
+define WHITE 1
+define BLUE 2
+
+define A(p, plvs) acc(p.l) && acc(Tree(p.l)) && vals(p.l) == plvs[1..]
+    define B acc(Tree(x)) && vals(x) == old(vals(x))[1..]
\ No newline at end of file
diff --git a/src/test/resources/reformatter/macros_expected.vpr b/src/test/resources/reformatter/macros_expected.vpr
new file mode 100644
index 000000000..160449e52
--- /dev/null
+++ b/src/test/resources/reformatter/macros_expected.vpr
@@ -0,0 +1,15 @@
+define access5(a) forall j: Int ::
+    0 <= j && j < len(a) ==> acc(loc(a, j).val)
+
+/**
+ * In the book, they use 'type PQueue = BraunTree'. This is not possible in 
+ * Viper. Therefore we will be using a macro to alias PQueue with BraunTree.
+ * This will allow us to follow the book more closely.
+ */
+define PQueue BraunTree
+
+define WHITE 1
+define BLUE 2
+
+define A(p, plvs) acc(p.l) && acc(Tree(p.l)) && vals(p.l) == plvs[1..]
+define B acc(Tree(x)) && vals(x) == old(vals(x))[1..]
\ No newline at end of file
diff --git a/src/test/resources/reformatter/methods.vpr b/src/test/resources/reformatter/methods.vpr
new file mode 100644
index 000000000..b8770b423
--- /dev/null
+++ b/src/test/resources/reformatter/methods.vpr
@@ -0,0 +1,139 @@
+method long_method(parameter_1: Int, parameter_2: Int, parameter_3: Int) {
+    var i: Int := 3;
+    
+    var j: Int := 3;
+    var k: Int := 3;
+}
+
+// This is another comment.
+/* This is a block-level commeny
+that spans
+over multiple lines   */
+method simple(n: Int, r: Bool) {}
+
+// This is a comment.
+method sum(nn: Int) returns (res: Int)
+    requires true
+    // A comment in-between.
+    requires /* A comment here */ true requires true
+    requires true
+    ensures true
+    ensures true
+    ensures true
+{}
+
+method sum2(n: Int) returns (res: Int)
+    requires 0 <= n
+    ensures res == n * (n + 1) / 2
+{
+    res := 0
+    var i: Int := 0;
+    while(i <= n) 
+        invariant i <= (n + 1)
+        invariant res == (i - 1) * i / 2
+    {
+        res := res + i
+        i := i + 1
+    }
+}
+
+method setTuple(this: Ref, l: Int, r: Int)
+    requires tuple(this)
+    ensures tuple(this)
+{
+    unfold tuple(this)
+    this.left := l
+    this.right := r
+    fold tuple(this)
+}
+
+method addTuple(this: Ref) returns (summ: Int)
+    requires acc(tuple(this), 1 / 2)
+    ensures acc(tuple(this), 1 / 2)
+{
+    unfold acc(tuple(this), 1 / 2)
+    summ := this.left + this.right
+    fold acc(tuple(this), 1 / 2)
+}
+
+method exclusivity(x: Ref, y: Ref) {
+    inhale acc(x.f)
+    inhale acc(y.f)
+    exhale x != y
+}
+
+method client(a1: Ref, b1: Ref) {
+    inhale acc(a1.f1) && acc(b1.f1)
+    a1.f1 := 1
+    b1.f1 := 3
+    inc(a1, 3)
+    assert b1.f1 == 3
+}
+
+method addTuple2(this1: Ref) returns (sum1: Int)
+    requires acc(tuple2(this1), 1/2)
+    ensures acc(tuple2(this1), 1/2)
+{
+    unfold acc(tuple2(this1), 1 / 2)
+    sum1 := this1.left1 + this1.right1
+    fold acc(tuple2(this1), 1 / 2)
+}
+
+method append(this: Ref, e: Int)
+    requires list(this)
+    ensures list(this)
+{
+    unfold list(this)
+    if (this.next3 == null) {
+        var n: Ref
+        n := new(elem3, next3)
+        n.elem3 := e
+        
+        n.next3 := null
+        this.next3 := n
+        fold list(n)
+    } else {
+        append(this.next3, e)
+    }
+    fold list(this)
+}
+
+method removeFirst(first: Ref, last: Ref, values: Seq[Int]) returns (value: Int, second: Ref) requires lseg(first, last, values) requires first != last ensures lseg(second, last, values[1..])
+{
+    unfold lseg(first, last, values)
+    value := first.elem4
+    second := first.next4
+}
+
+method client1(a: MyType1[Bool, Ref])
+    requires a == bin_oper1(a, a)
+{
+    var a: Map[K, V]
+    var b: MyType1[Int, Bool] := constructor_a1(11)
+    var c: MyType1[Int, Bool] := constructor_b1(true)
+    var d: MyType1[Int, Bool] := bin_oper1(b, c)
+}
+
+method decreasesTuple()
+    decreases true, true, true, true if true
+{}
+
+method decreases2()
+    decreases _ if true
+{}
+
+method empty_assign() {
+/* A sample comment.
+   */
+    
+    swap(a, pivotIndex, right)
+}
+
+method with_inhale_exhale(lock: Ref)
+    ensures [true,forperm r: Ref [r.held] :: false]
+    
+method package_wand(lock: Ref) {
+    package A(p, plvs) --* B{
+        fold acc(Tree(p))
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/methods_expected.vpr b/src/test/resources/reformatter/methods_expected.vpr
new file mode 100644
index 000000000..eeea333e0
--- /dev/null
+++ b/src/test/resources/reformatter/methods_expected.vpr
@@ -0,0 +1,143 @@
+method long_method(parameter_1: Int, parameter_2: Int, parameter_3: Int) {
+    var i: Int := 3;
+    
+    var j: Int := 3;
+    var k: Int := 3;
+}
+
+// This is another comment.
+/* This is a block-level commeny
+that spans
+over multiple lines   */
+method simple(n: Int, r: Bool) {}
+
+// This is a comment.
+method sum(nn: Int) returns (res: Int)
+    requires true
+    // A comment in-between.
+    requires /* A comment here */ true
+    requires true
+    requires true
+    ensures true
+    ensures true
+    ensures true
+{}
+
+method sum2(n: Int) returns (res: Int)
+    requires 0 <= n
+    ensures res == n * (n + 1) / 2
+{
+    res := 0
+    var i: Int := 0;
+    while (i <= n)
+        invariant i <= (n + 1)
+        invariant res == (i - 1) * i / 2
+    {
+        res := res + i
+        i := i + 1
+    }
+}
+
+method setTuple(this: Ref, l: Int, r: Int)
+    requires tuple(this)
+    ensures tuple(this)
+{
+    unfold tuple(this)
+    this.left := l
+    this.right := r
+    fold tuple(this)
+}
+
+method addTuple(this: Ref) returns (summ: Int)
+    requires acc(tuple(this), 1 / 2)
+    ensures acc(tuple(this), 1 / 2)
+{
+    unfold acc(tuple(this), 1 / 2)
+    summ := this.left + this.right
+    fold acc(tuple(this), 1 / 2)
+}
+
+method exclusivity(x: Ref, y: Ref) {
+    inhale acc(x.f)
+    inhale acc(y.f)
+    exhale x != y
+}
+
+method client(a1: Ref, b1: Ref) {
+    inhale acc(a1.f1) && acc(b1.f1)
+    a1.f1 := 1
+    b1.f1 := 3
+    inc(a1, 3)
+    assert b1.f1 == 3
+}
+
+method addTuple2(this1: Ref) returns (sum1: Int)
+    requires acc(tuple2(this1), 1 / 2)
+    ensures acc(tuple2(this1), 1 / 2)
+{
+    unfold acc(tuple2(this1), 1 / 2)
+    sum1 := this1.left1 + this1.right1
+    fold acc(tuple2(this1), 1 / 2)
+}
+
+method append(this: Ref, e: Int)
+    requires list(this)
+    ensures list(this)
+{
+    unfold list(this)
+    if (this.next3 == null) {
+        var n: Ref
+        n := new(elem3, next3)
+        n.elem3 := e
+        
+        n.next3 := null
+        this.next3 := n
+        fold list(n)
+    } else {
+        append(this.next3, e)
+    }
+    fold list(this)
+}
+
+method removeFirst(first: Ref, last: Ref, values: Seq[Int]) returns (value: Int, second: Ref)
+    requires lseg(first, last, values)
+    requires first != last
+    ensures lseg(second, last, values[1..])
+{
+    unfold lseg(first, last, values)
+    value := first.elem4
+    second := first.next4
+}
+
+method client1(a: MyType1[Bool, Ref])
+    requires a == bin_oper1(a, a)
+{
+    var a: Map[K, V]
+    var b: MyType1[Int, Bool] := constructor_a1(11)
+    var c: MyType1[Int, Bool] := constructor_b1(true)
+    var d: MyType1[Int, Bool] := bin_oper1(b, c)
+}
+
+method decreasesTuple()
+    decreases true, true, true, true if true
+{}
+
+method decreases2()
+    decreases _ if true
+{}
+
+method empty_assign() {
+    /* A sample comment.
+   */
+    
+    swap(a, pivotIndex, right)
+}
+
+method with_inhale_exhale(lock: Ref)
+    ensures [true, forperm r: Ref [r.held] :: false]
+
+method package_wand(lock: Ref) {
+    package A(p, plvs) --* B {
+        fold acc(Tree(p))
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/not_working.vpr b/src/test/resources/reformatter/not_working.vpr
new file mode 100644
index 000000000..d5a7cdb3d
--- /dev/null
+++ b/src/test/resources/reformatter/not_working.vpr
@@ -0,0 +1,29 @@
+// This test demonstrates three code snippets which are (to the best of my
+// knowledge) the only very big limitations to the current version of the
+// formatter, and unfortunately fixing them is very difficult with the current
+// architecture of the reformatter, since we have limited flexibility due to the
+// fact that we rely on `PrettyPrintPrimitives` instead of having a hand-written
+// reformatter.
+
+method test1() {
+    // Problem 1: The side comment will be pushed to the next line.
+    // The reason for this is that we separate variables with a newline by
+    // default, and since the newline will be added before adding the trivia,
+    // the newline will be added before the comment, and thus move to the next
+    // line.
+    var a: Int := 1; // A side comment
+    // Problem 2: The 4 in the next line will not be indented.
+    var b: Int := 2 + // Another comment
+    4
+}
+
+// Problem 3: Trailing comments might not be indented correctly.
+// In this case, since we always attach the trivia to the next node below
+// (the closing bracket in this case), it will also be subject to the indentation
+// of that node.
+method c() {
+    if (true) {
+        var b: Int := 3;
+    }
+    // A trailing comment
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/not_working_expected.vpr b/src/test/resources/reformatter/not_working_expected.vpr
new file mode 100644
index 000000000..9206aa5d3
--- /dev/null
+++ b/src/test/resources/reformatter/not_working_expected.vpr
@@ -0,0 +1,30 @@
+// This test demonstrates three code snippets which are (to the best of my
+// knowledge) the only very big limitations to the current version of the
+// formatter, and unfortunately fixing them is very difficult with the current
+// architecture of the reformatter, since we have limited flexibility due to the
+// fact that we rely on `PrettyPrintPrimitives` instead of having a hand-written
+// reformatter.
+
+method test1() {
+    // Problem 1: The side comment will be pushed to the next line.
+    // The reason for this is that we separate variables with a newline by
+    // default, and since the newline will be added before adding the trivia,
+    // the newline will be added before the comment, and thus move to the next
+    // line.
+    var a: Int := 1;
+    // A side comment
+    // Problem 2: The 4 in the next line will not be indented.
+    var b: Int := 2 + // Another comment
+4
+}
+
+// Problem 3: Trailing comments might not be indented correctly.
+// In this case, since we always attach the trivia to the next node below
+// (the closing bracket in this case), it will also be subject to the indentation
+// of that node.
+method c() {
+    if (true) {
+        var b: Int := 3;
+    }
+// A trailing comment
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/predicates.vpr b/src/test/resources/reformatter/predicates.vpr
new file mode 100644
index 000000000..428064344
--- /dev/null
+++ b/src/test/resources/reformatter/predicates.vpr
@@ -0,0 +1,19 @@
+predicate tuple(this: Ref) {
+    acc(this.left) && acc(this.right)
+}
+
+predicate tuple2(this: Ref) {
+    acc(this.left1) && acc(this.right1)
+}
+
+predicate list(this: Ref) {
+    acc(this.elem3) && acc(this.next3) && (this.next3 != null ==> list(this.next3))
+}
+
+predicate lseg(first: Ref, last: Ref, values: Seq[Int]) {
+    first != last ==> acc(first.elem4) && acc(first.next4) && 0 < |values| && first.elem4 == values[0] && lseg(first.next4, last, values[1..])
+}
+
+predicate list5(this: Ref) {
+    acc(this.elem5) && acc(this.next5) && (this.next5 != null ==> list5(this.next5))
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/predicates_expected.vpr b/src/test/resources/reformatter/predicates_expected.vpr
new file mode 100644
index 000000000..241293f64
--- /dev/null
+++ b/src/test/resources/reformatter/predicates_expected.vpr
@@ -0,0 +1,25 @@
+predicate tuple(this: Ref) {
+    acc(this.left) && acc(this.right)
+}
+
+predicate tuple2(this: Ref) {
+    acc(this.left1) && acc(this.right1)
+}
+
+predicate list(this: Ref) {
+    acc(this.elem3)
+    && acc(this.next3) && (this.next3 != null ==> list(this.next3))
+}
+
+predicate lseg(first: Ref, last: Ref, values: Seq[Int]) {
+    first != last ==>
+        acc(first.elem4)
+        && acc(first.next4)
+        && 0 < |values|
+        && first.elem4 == values[0] && lseg(first.next4, last, values[1..])
+}
+
+predicate list5(this: Ref) {
+    acc(this.elem5)
+    && acc(this.next5) && (this.next5 != null ==> list5(this.next5))
+}
\ No newline at end of file
diff --git a/src/test/resources/reformatter/trailing_comment.vpr b/src/test/resources/reformatter/trailing_comment.vpr
new file mode 100644
index 000000000..99fa1619d
--- /dev/null
+++ b/src/test/resources/reformatter/trailing_comment.vpr
@@ -0,0 +1,2 @@
+field f: Int
+// This is a trailing comment
\ No newline at end of file
diff --git a/src/test/resources/reformatter/trailing_comment_expected.vpr b/src/test/resources/reformatter/trailing_comment_expected.vpr
new file mode 100644
index 000000000..99fa1619d
--- /dev/null
+++ b/src/test/resources/reformatter/trailing_comment_expected.vpr
@@ -0,0 +1,2 @@
+field f: Int
+// This is a trailing comment
\ No newline at end of file
diff --git a/src/test/scala/ASTTransformationTests.scala b/src/test/scala/ASTTransformationTests.scala
index d3a6ec517..5265c64ec 100644
--- a/src/test/scala/ASTTransformationTests.scala
+++ b/src/test/scala/ASTTransformationTests.scala
@@ -84,11 +84,11 @@ class ASTTransformationTests extends AnyFunSuite {
      val p = (NoPosition, NoPosition)
      val binExp1 = PBinExp(PIntLit(1)(p), PReserved.implied(PSymOp.EqEq), PIntLit(1)(p))(p)
      val method1 = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp1)(p))))(p)))(p)
-     val original = PProgram(Nil, Seq(method1))(p, Seq())
+     val original = PProgram(Nil, Seq(method1))(p, Seq(), Seq(), "")
 
      val binExp2 = PBinExp(PIntLit(3)(p), PReserved.implied(PSymOp.EqEq), PIntLit(3)(p))(p)
      val method2 = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp2)(p))))(p)))(p)
-     val target = PProgram(Nil, Seq(method2))(p, Seq())
+     val target = PProgram(Nil, Seq(method2))(p, Seq(), Seq(), "")
 
      case class Context(increment: Int)
 
@@ -124,11 +124,11 @@ class ASTTransformationTests extends AnyFunSuite {
     val function = PFunction(Seq(), PReserved.implied(PKw.Function), PIdnDef("f")(p), commaParen(Seq(PFormalArgDecl(PIdnDef("x")(p), PReserved.implied(PSym.Colon), TypeHelper.Int)(p), PFormalArgDecl(PIdnDef("y")(p), PReserved.implied(PSym.Colon), TypeHelper.Int)(p))), PReserved.implied(PSym.Colon), TypeHelper.Int, PDelimited.empty, PDelimited.empty, None)(p)
     val assume1 = PAssume(PReserved.implied(PKw.Assume), PBinExp(PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(1)(p), PIntLit(1)(p))), None)(p), PReserved.implied(PSymOp.EqEq), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(1)(p), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(1)(p), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(1)(p), PIntLit(1)(p))), None)(p))), None)(p))), None)(p))(p))(p)
     val method1 = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(PSeqn(PDelimited.impliedBlock(Seq(assume1)))(p)))(p)
-    val original = PProgram(Nil, Seq(function, method1))(p, Seq())
+    val original = PProgram(Nil, Seq(function, method1))(p, Seq(), Seq(), "")
 
     val assume2 = PAssume(PReserved.implied(PKw.Assume), PBinExp(PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(2)(p), PIntLit(1)(p))), None)(p), PReserved.implied(PSymOp.EqEq), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(2)(p), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(3)(p), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(4)(p), PIntLit(1)(p))), None)(p))), None)(p))), None)(p))(p))(p)
     val method2 = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(PSeqn(PDelimited.impliedBlock(Seq(assume2)))(p)))(p)
-    val target = PProgram(Nil, Seq(function, method2))(p, Seq())
+    val target = PProgram(Nil, Seq(function, method2))(p, Seq(), Seq(), "")
 
     case class Context(increment: Int)
 
@@ -149,7 +149,7 @@ class ASTTransformationTests extends AnyFunSuite {
     val p = (NoPosition, NoPosition)
     val requires = PForall(PReserved.implied(PKw.Forall), PDelimited.implied(Seq(PLogicalVarDecl(PIdnDef("y")(p), PReserved.implied(PSym.Colon), TypeHelper.Int)(p)), PReserved.implied(PSym.Comma)), PReserved.implied(PSym.ColonColon), Seq(), PBinExp(PIdnUseExp("y")(p), PReserved.implied(PSymOp.EqEq), PIdnUseExp("y")(p))(p))(p)
     val function = PFunction(Seq(), PReserved.implied(PKw.Function), PIdnDef("f")(p), PDelimited.impliedParenComma(Seq(PFormalArgDecl(PIdnDef("x")(p), PReserved.implied(PSym.Colon), TypeHelper.Ref)(p))), PReserved.implied(PSym.Colon), TypeHelper.Bool, PDelimited.implied(Seq(PSpecification(PReserved.implied(PKw.Requires), requires)(p)), None), PDelimited.empty, None)(p)
-    val program = PProgram(Nil, Seq(function))(p, Seq())
+    val program = PProgram(Nil, Seq(function))(p, Seq(), Seq(), "")
 
     case class Context()
 
diff --git a/src/test/scala/PluginTests.scala b/src/test/scala/PluginTests.scala
index 1f34f2ef3..dfafef508 100644
--- a/src/test/scala/PluginTests.scala
+++ b/src/test/scala/PluginTests.scala
@@ -121,7 +121,7 @@ class TestPluginAddPredicate extends SilverPlugin {
     PProgram(
       input.imported,
       input.members :+ PPredicate(Seq(), PReserved.implied(PKw.Predicate), PIdnDef("testPredicate")(p), PGrouped.impliedParen(PDelimited.empty), None)(p),
-    )(input.pos, input.localErrors)
+    )(input.pos, input.localErrors, input.offsets, input.rawProgram)
   }
 
   /** Called after methods are filtered but before the verification by the backend happens.
diff --git a/src/test/scala/ReformatterTests.scala b/src/test/scala/ReformatterTests.scala
new file mode 100644
index 000000000..a88773cb8
--- /dev/null
+++ b/src/test/scala/ReformatterTests.scala
@@ -0,0 +1,85 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2024 ETH Zurich.
+
+import org.scalatest.funsuite.AnyFunSuite
+import viper.silver.frontend._
+import viper.silver.ast.utility.DiskLoader
+import viper.silver.parser.{PProgram, ReformatPrettyPrinter}
+import viper.silver.reporter.StdIOReporter
+
+import java.nio.file.{Path, Paths}
+
+class ReformatterTests extends AnyFunSuite {
+  object Provider extends ReformatterAstProvider(StdIOReporter()) {
+    def parse(content: String): PProgram = {
+      doParsing(content) match {
+        case Succ(r) => r
+      }
+    }
+
+    def setInput(path: Path): Unit = {
+      _inputFile = Some(path)
+    }
+  }
+
+  def check_inner(name: String): Unit = {
+    val input_path = Paths.get(getClass.getResource("reformatter/" + name + ".vpr").toURI)
+    val expected_path = Paths.get(getClass.getResource("reformatter/" + name + "_expected.vpr").toURI)
+
+    val inputProgram = DiskLoader.loadContent(input_path).get
+    Provider.setInput(input_path)
+    val ast = Provider.parse(inputProgram)
+
+    val reformatted = ReformatPrettyPrinter.reformatProgram(ast);
+    val expected = DiskLoader.loadContent(expected_path).get
+
+    assert(reformatted == expected)
+  }
+
+  test(s"adts") {
+    check_inner("adts")
+  }
+
+  test(s"annotations") {
+    check_inner("annotations")
+  }
+
+  test(s"domains") {
+    check_inner("domains")
+  }
+
+  test(s"expressions") {
+    check_inner("expressions")
+  }
+
+  test(s"fields") {
+    check_inner("fields")
+  }
+
+  test(s"functions") {
+    check_inner("functions")
+  }
+
+  test(s"macros") {
+    check_inner("macros")
+  }
+
+  test(s"methods") {
+    check_inner("methods")
+  }
+
+  test(s"predicates") {
+    check_inner("predicates")
+  }
+
+  test(s"trailing_comment") {
+    check_inner("trailing_comment")
+  }
+
+  test(s"not_working") {
+    check_inner("not_working")
+  }
+}
\ No newline at end of file
diff --git a/src/test/scala/SemanticAnalysisTests.scala b/src/test/scala/SemanticAnalysisTests.scala
index 2d9ace8e5..0bf5f6249 100644
--- a/src/test/scala/SemanticAnalysisTests.scala
+++ b/src/test/scala/SemanticAnalysisTests.scala
@@ -31,7 +31,7 @@ class SemanticAnalysisTests extends AnyFunSuite {
     val binExp2 = PBinExp(PIntLit(1)(p), PReserved.implied(PSymOp.EqEq), PIntLit(1)(p))(p)
     val body = PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp1)(p), PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp2)(p))))(p))))(p)
     val method = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(body))(p)
-    val program = PProgram(Nil, Seq(method))(p, Seq())
+    val program = PProgram(Nil, Seq(method))(p, Seq(), Seq(), "")
     assert(frontend.doSemanticAnalysis(program) === frontend.Succ(program))
   }
 
@@ -40,7 +40,7 @@ class SemanticAnalysisTests extends AnyFunSuite {
     val binExp = PBinExp(PIntLit(1)(p), PReserved.implied(PSymOp.EqEq), PIntLit(1)(p))(p)
     val body = PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp)(p), PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp)(p))))(p))))(p)
     val method = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(body))(p)
-    val program = PProgram(Nil, Seq(method))(p, Seq())
+    val program = PProgram(Nil, Seq(method))(p, Seq(), Seq(), "")
     assert(frontend.doSemanticAnalysis(program) === frontend.Succ(program))
   }
 }