From ce22bac6d5fa1c0e9d30a71bd4b913efa838eaa1 Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 26 Feb 2024 13:18:04 +0100
Subject: [PATCH 01/14] Allow annotations to be placed before specification
 keywords

---
 .../viper/silver/parser/FastParser.scala      | 26 ++++++++++++++++---
 1 file changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 1502bf1ac..a37f73214 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -809,7 +809,16 @@ class FastParser {
   def whileStmt[$: P]: P[PKw.While => Pos => PWhile] =
     P((parenthesizedExp ~~ semiSeparated(invariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile(_, cond, invs, body) })
 
-  def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] = P((P(PKw.Invariant) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.invSpecification(ctx))
+  // TODO does this handle positions correctly/consistently?
+  // TODO is the look-ahead &(...) really necessary, or can one ensure backtracking in a cleaner way?
+  // see also annotatedPrecondition, annotatedPostcondition
+  def annotatedInvariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
+    P(&(annotation ~ invariant) ~ annotation ~ invariant).map{ case (ann, spec) => p: (FilePosition, FilePosition) =>
+      new PSpecification[PKw.InvSpec](spec.k, PAnnotatedExp(ann, spec.e)(p))(p) }.pos
+
+  def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
+    P(annotatedInvariant | (P(PKw.Invariant) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.invSpecification(ctx))
+    // P((P(PKw.Invariant) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.invSpecification(ctx))
 
   def localVars[$: P]: P[PKw.Var => Pos => PVars] =
     P((nonEmptyIdnTypeList(PLocalVarDecl(_)) ~~~ (P(PSymOp.Assign) ~ exp).lw.?) map { case (a, i) => PVars(_, a, i) })
@@ -920,10 +929,21 @@ class FastParser {
       ap: PAnnotationsPosition => PFunction(ap.annotations, k, idn, args, c, typ, d, e, f)(ap.pos)
   })
 
+  def annotatedPrecondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
+    P(&(annotation ~ precondition) ~ annotation ~ precondition).map{ case (ann, spec) => p: (FilePosition, FilePosition) =>
+      new PSpecification[PKw.PreSpec](spec.k, PAnnotatedExp(ann, spec.e)(p))(p) }.pos // p or spec.pos?
+
+  def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
+    P((P(PKw.Requires) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.preSpecification(ctx) | annotatedPrecondition)
+    // P((P(PKw.Requires) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.preSpecification(ctx))
 
-  def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] = P((P(PKw.Requires) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.preSpecification(ctx))
+  def annotatedPostcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
+    P(&(annotation ~ postcondition) ~ annotation ~ postcondition).map{ case (ann, spec) => p: (FilePosition, FilePosition) =>
+      new PSpecification[PKw.PostSpec](spec.k, PAnnotatedExp(ann, spec.e)(p))(p) }.pos
 
-  def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] = P((P(PKw.Ensures) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.postSpecification(ctx))
+  def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
+    P((P(PKw.Ensures) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.postSpecification(ctx) | annotatedPostcondition)
+    // P((P(PKw.Ensures) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.postSpecification(ctx))
 
   def predicateDecl[$: P]: P[PKw.Predicate => PAnnotationsPosition => PPredicate] = P(idndef ~ argList(formalArg) ~~~ bracedExp.lw.?).map {
     case (idn, args, c) => k =>

From 2df97a73d6460d81e4c6f51ab7d8c49759b2f6fb Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 26 Feb 2024 13:47:38 +0100
Subject: [PATCH 02/14] Parse ///-docstring as annotation WIP

---
 .../scala/viper/silver/parser/FastParser.scala  | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index a37f73214..f90d66a28 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -30,9 +30,11 @@ object FastParserCompanion {
       NoTrace((" " | "\t").rep)
   }
 
+  // TODO why is this duplicated? see FastParser below
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
+      // NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
       NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
@@ -315,9 +317,11 @@ class FastParser {
   import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym}
 
 
+  // TODO why is this duplicated? see FastParserCompanion
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
+      // NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
       NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
@@ -403,6 +407,19 @@ class FastParser {
 
   def stringLiteral[$: P]: P[PStringLiteral] = P((CharsWhile(_ != '\"').! map PRawString.apply).pos.quotes map (PStringLiteral.apply _)).pos
 
+  // it might be preferable to remove this and instead do a preprocessing step inside the doc plugin
+  // which replaces '///some docstring' by the corresponding annotation '@doc("some docstring")'
+  // TODO does the position make sense?
+  def docAnnotation[$: P]: P[PAnnotation] = P("///" ~~ CharsWhile(_ != '\n', 0).!).map{
+    case s: String => p: (FilePosition, FilePosition) =>
+      val annotationParser: P[_] => P[PAnnotation] = annotation(_)
+      fastparse.parse("@doc(\"" + s + "\")", annotationParser) match {
+        case Parsed.Success(ann, _) => new PAnnotation(ann.at, ann.key, ann.values)(p)
+        case Parsed.Failure(_, _, _) => throw new Exception("parsing ///-annotation failed") // this should not happen
+      }
+  }.pos
+
+  // def annotation[$: P]: P[PAnnotation] = P(docAnnotation) | P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos
   def annotation[$: P]: P[PAnnotation] = P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos
 
   def annotated[$: P, T](inner: => P[PAnnotationsPosition => T]): P[T] = P((annotation.rep(0) ~ inner).map {

From 4509a307bf06c71ace3bc4b097b02305f6df98d0 Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 4 Mar 2024 08:25:15 +0100
Subject: [PATCH 03/14] Enable ///-parsing, fix ambiguity with division

---
 .../scala/viper/silver/parser/FastParser.scala     | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index f90d66a28..4ac2b81a8 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -34,8 +34,8 @@ object FastParserCompanion {
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
-      // NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      // NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
   def identStarts[$: P] = CharIn("A-Z", "a-z", "$_")
@@ -321,8 +321,8 @@ class FastParser {
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
-      // NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      // NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
   implicit val lineCol: LineCol = new LineCol(this)
@@ -407,9 +407,7 @@ class FastParser {
 
   def stringLiteral[$: P]: P[PStringLiteral] = P((CharsWhile(_ != '\"').! map PRawString.apply).pos.quotes map (PStringLiteral.apply _)).pos
 
-  // it might be preferable to remove this and instead do a preprocessing step inside the doc plugin
-  // which replaces '///some docstring' by the corresponding annotation '@doc("some docstring")'
-  // TODO does the position make sense?
+  // TODO check positions
   def docAnnotation[$: P]: P[PAnnotation] = P("///" ~~ CharsWhile(_ != '\n', 0).!).map{
     case s: String => p: (FilePosition, FilePosition) =>
       val annotationParser: P[_] => P[PAnnotation] = annotation(_)
@@ -503,7 +501,7 @@ class FastParser {
 
   def suffixExpr[$: P](bracketed: Boolean = false): P[PExp] = P((atomParen(bracketed) ~~~ suffix.lw.rep).map { case (fac, ss) => foldPExp(fac, ss) })
 
-  def termOp[$: P] = P(reservedSymMany(None, StringIn("*", "/", "\\", "%"), _ match {
+  def termOp[$: P] = P(reservedSymMany(None, !("///") ~ StringIn("*", "/", "\\", "%"), _ match {
     case "*" => PSymOp.Mul
     case "/" => PSymOp.Div
     case "\\" => PSymOp.ArithDiv

From 725ef22ac7ab37ef8300a6e8bd379486fbf88ce7 Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 4 Mar 2024 10:29:37 +0100
Subject: [PATCH 04/14] Directly construct docAnnotations

---
 src/main/scala/viper/silver/parser/FastParser.scala | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 4ac2b81a8..aa574d652 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -410,11 +410,12 @@ class FastParser {
   // TODO check positions
   def docAnnotation[$: P]: P[PAnnotation] = P("///" ~~ CharsWhile(_ != '\n', 0).!).map{
     case s: String => p: (FilePosition, FilePosition) =>
-      val annotationParser: P[_] => P[PAnnotation] = annotation(_)
-      fastparse.parse("@doc(\"" + s + "\")", annotationParser) match {
-        case Parsed.Success(ann, _) => new PAnnotation(ann.at, ann.key, ann.values)(p)
-        case Parsed.Failure(_, _, _) => throw new Exception("parsing ///-annotation failed") // this should not happen
-      }
+      val annotationKey = PRawString("doc")(NoPosition, NoPosition)
+      val docstring = PStringLiteral(PGrouped.apply[PSym.Quote.type, PRawString]
+                                       (PReserved.implied(PSym.Quote), PRawString(s)(NoPosition, NoPosition), PReserved.implied(PSym.Quote))
+                                                   (NoPosition, NoPosition))(NoPosition, NoPosition)
+      val annotationValues = PDelimited.implied[PStringLiteral, PSym.Comma](Seq(docstring), PReserved.implied(PSym.Comma))
+      PAnnotation(at = PReserved.implied(PSym.At), key = annotationKey, values = PGrouped.impliedParen(annotationValues))(p)
   }.pos
 
   // def annotation[$: P]: P[PAnnotation] = P(docAnnotation) | P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos

From 2469a2e37d7b98f3b6112ed87f337eb6b3313d94 Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 4 Mar 2024 11:16:20 +0100
Subject: [PATCH 05/14] Add annotations to specification nodes in the Parse AST

---
 .../viper/silver/parser/FastParser.scala      | 36 +++++++++----------
 .../scala/viper/silver/parser/ParseAst.scala  |  2 +-
 .../termination/TerminationPlugin.scala       |  7 ++--
 3 files changed, 22 insertions(+), 23 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index aa574d652..6d93f7a29 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -418,8 +418,7 @@ class FastParser {
       PAnnotation(at = PReserved.implied(PSym.At), key = annotationKey, values = PGrouped.impliedParen(annotationValues))(p)
   }.pos
 
-  // def annotation[$: P]: P[PAnnotation] = P(docAnnotation) | P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos
-  def annotation[$: P]: P[PAnnotation] = P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos
+  def annotation[$: P]: P[PAnnotation] = P(P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos | docAnnotation)
 
   def annotated[$: P, T](inner: => P[PAnnotationsPosition => T]): P[T] = P((annotation.rep(0) ~ inner).map {
     case (annotations, i) => pos: Pos => i(PAnnotationsPosition(annotations, pos))
@@ -823,18 +822,17 @@ class FastParser {
     P((P(PKw.Else) ~ stmtBlock()) map (PElse.apply _).tupled).pos
 
   def whileStmt[$: P]: P[PKw.While => Pos => PWhile] =
-    P((parenthesizedExp ~~ semiSeparated(invariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile(_, cond, invs, body) })
+    P((parenthesizedExp ~~ semiSeparated(annotatedInvariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile(_, cond, invs, body) })
 
   // TODO does this handle positions correctly/consistently?
-  // TODO is the look-ahead &(...) really necessary, or can one ensure backtracking in a cleaner way?
   // see also annotatedPrecondition, annotatedPostcondition
   def annotatedInvariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
-    P(&(annotation ~ invariant) ~ annotation ~ invariant).map{ case (ann, spec) => p: (FilePosition, FilePosition) =>
-      new PSpecification[PKw.InvSpec](spec.k, PAnnotatedExp(ann, spec.e)(p))(p) }.pos
+    P(annotation.rep(0) ~ invariant).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+            PSpecification[PKw.InvSpec](spec.k, spec.e, anns)(p) }.pos
 
   def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
-    P(annotatedInvariant | (P(PKw.Invariant) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.invSpecification(ctx))
-    // P((P(PKw.Invariant) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.invSpecification(ctx))
+    P((P(PKw.Invariant) ~ exp).map{ case (kw, e) => p: (FilePosition, FilePosition) =>
+      PSpecification[PKw.InvSpec](kw, e)(p) }.pos | ParserExtension.invSpecification(ctx))
 
   def localVars[$: P]: P[PKw.Var => Pos => PVars] =
     P((nonEmptyIdnTypeList(PLocalVarDecl(_)) ~~~ (P(PSymOp.Assign) ~ exp).lw.?) map { case (a, i) => PVars(_, a, i) })
@@ -849,7 +847,7 @@ class FastParser {
   def goto[$: P]: P[PKw.Goto => Pos => PGoto] = P(idnref[$, PLabel] map { i => PGoto(_, i) _ })
 
   def label[$: P]: P[PKw.Label => Pos => PLabel] =
-    P((idndef ~~ semiSeparated(invariant)) map { case (i, inv) => k=> PLabel(k, i, inv) _ })
+    P((idndef ~~ semiSeparated(annotatedInvariant)) map { case (i, inv) => k=> PLabel(k, i, inv) _ })
 
   def packageWand[$: P]: P[PKw.Package => Pos => PPackageWand] =
     P((magicWandExp() ~~~ stmtBlock().lw.?) map { case (wand, proof) => PPackageWand(_, wand, proof) _ })
@@ -940,26 +938,26 @@ class FastParser {
   })
 
   def functionDecl[$: P]: P[PKw.Function => PAnnotationsPosition => PFunction] = P((idndef ~ argList(formalArg) ~ PSym.Colon ~ typ
-    ~~ semiSeparated(precondition) ~~ semiSeparated(postcondition) ~~~ bracedExp.lw.?
+    ~~ semiSeparated(annotatedPrecondition) ~~ semiSeparated(annotatedPostcondition) ~~~ bracedExp.lw.?
   ) map { case (idn, args, c, typ, d, e, f) => k =>
       ap: PAnnotationsPosition => PFunction(ap.annotations, k, idn, args, c, typ, d, e, f)(ap.pos)
   })
 
   def annotatedPrecondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
-    P(&(annotation ~ precondition) ~ annotation ~ precondition).map{ case (ann, spec) => p: (FilePosition, FilePosition) =>
-      new PSpecification[PKw.PreSpec](spec.k, PAnnotatedExp(ann, spec.e)(p))(p) }.pos // p or spec.pos?
+    P(annotation.rep(0) ~ precondition).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+            PSpecification[PKw.PreSpec](spec.k, spec.e, anns)(p) }.pos
 
   def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
-    P((P(PKw.Requires) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.preSpecification(ctx) | annotatedPrecondition)
-    // P((P(PKw.Requires) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.preSpecification(ctx))
+    P((P(PKw.Requires) ~ exp).map{ case (kw, e) => p: (FilePosition, FilePosition) =>
+        PSpecification[PKw.PreSpec](kw, e)(p)}.pos | ParserExtension.preSpecification(ctx))
 
   def annotatedPostcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
-    P(&(annotation ~ postcondition) ~ annotation ~ postcondition).map{ case (ann, spec) => p: (FilePosition, FilePosition) =>
-      new PSpecification[PKw.PostSpec](spec.k, PAnnotatedExp(ann, spec.e)(p))(p) }.pos
+    P(annotation.rep(0) ~ postcondition).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+      PSpecification[PKw.PostSpec](spec.k, spec.e, anns)(p) }.pos
 
   def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
-    P((P(PKw.Ensures) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.postSpecification(ctx) | annotatedPostcondition)
-    // P((P(PKw.Ensures) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.postSpecification(ctx))
+    P((P(PKw.Ensures) ~ exp).map{ case (kw, e) => p: (FilePosition, FilePosition) =>
+        PSpecification[PKw.PostSpec](kw, e)(p)}.pos | ParserExtension.postSpecification(ctx))
 
   def predicateDecl[$: P]: P[PKw.Predicate => PAnnotationsPosition => PPredicate] = P(idndef ~ argList(formalArg) ~~~ bracedExp.lw.?).map {
     case (idn, args, c) => k =>
@@ -967,7 +965,7 @@ class FastParser {
   }
 
   def methodDecl[$: P]: P[PKw.Method => PAnnotationsPosition => PMethod] =
-    P((idndef ~ argList(formalArg) ~~~ methodReturns.lw.? ~~ semiSeparated(precondition) ~~ semiSeparated(postcondition) ~~~ stmtBlock().lw.?) map {
+    P((idndef ~ argList(formalArg) ~~~ methodReturns.lw.? ~~ semiSeparated(annotatedPrecondition) ~~ semiSeparated(annotatedPostcondition) ~~~ stmtBlock().lw.?) map {
         case (idn, args, rets, pres, posts, body) => k =>
           ap: PAnnotationsPosition => PMethod(ap.annotations, k, idn, args, rets, pres, posts, body)(ap.pos)
     })
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 539a80fa8..920b98246 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1668,7 +1668,7 @@ case class PFields(annotations: Seq[PAnnotation], field: PKw.Field, fields: PDel
   override def declares: Seq[PGlobalDeclaration] = fields.toSeq
 }
 
-case class PSpecification[+T <: PKw.Spec](k: PReserved[PKw.Spec], e: PExp)(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
+case class PSpecification[+T <: PKw.Spec](k: PReserved[PKw.Spec], e: PExp, annotations: Seq[PAnnotation] = Seq())(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
   override def pretty: String = "\n  " + super.pretty
 }
 
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 a77b9ff91..519972442 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -8,7 +8,7 @@ package viper.silver.plugin.standard.termination
 
 import viper.silver.ast.utility.{Functions, ViperStrategy}
 import viper.silver.ast.utility.rewriter.{SimpleContext, Strategy, StrategyBuilder}
-import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, FuncApp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
+import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, FilePosition, FuncApp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
 import viper.silver.parser._
 import viper.silver.plugin.standard.predicateinstance.{PMarkerSymbol, PPredicateInstance}
 import viper.silver.plugin.standard.termination.transformation.Trafo
@@ -45,7 +45,8 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
    * decreases *
    */
   def decreases[$: P]: P[PSpecification[PDecreasesKeyword.type]] =
-    P((P(PDecreasesKeyword) ~ (decreasesWildcard | decreasesStar | decreasesTuple)) map (PSpecification.apply _).tupled).pos
+    P((P(PDecreasesKeyword) ~ (decreasesWildcard | decreasesStar | decreasesTuple)) map {
+        case (k, e) => p: (FilePosition, FilePosition) => PSpecification(k, e)(p) }).pos
   def decreasesTuple[$: P]: P[PDecreasesTuple] =
     P((exp.delimited(PSym.Comma) ~~~ condition.lw.?) map (PDecreasesTuple.apply _).tupled).pos
   def decreasesWildcard[$: P]: P[PDecreasesWildcard] = P((P(PWildcardSym) ~~~ condition.lw.?) map (PDecreasesWildcard.apply _).tupled).pos
@@ -239,7 +240,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
    * Remove decreases clauses from the AST and add them as information to the AST nodes
    */
   override def beforeVerify(input: Program): Program = {
-    // Prevent potentially unsafe (mutually) recursive function calls in function postcondtions
+    // Prevent potentially unsafe (mutually) recursive function calls in function postconditions
     // for all functions that don't have a decreases clause
     if (!deactivated) {
       lazy val cycles = Functions.findFunctionCyclesViaOptimized(input, func => func.body.toSeq)

From 4149349686ef108eea8002333067ad6ef3a77d4d Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 4 Mar 2024 11:25:51 +0100
Subject: [PATCH 06/14] Move specification annotations to their expressions in
 Viper AST

---
 .../scala/viper/silver/parser/Translator.scala     | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index ecc2fc4ec..3d131c38e 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -81,7 +81,9 @@ case class Translator(program: PProgram) {
 
       val newBody = body.map(actualBody => stmt(actualBody).asInstanceOf[Seqn])
 
-      val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(m.pos, m.info, m.errT)
+      val finalMethod = m.copy(pres = pres.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                               posts = posts.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                               body = newBody)(m.pos, m.info, m.errT)
 
       members(m.name) = finalMethod
 
@@ -107,7 +109,9 @@ case class Translator(program: PProgram) {
   private def translate(f: PFunction): Function = f match {
     case PFunction(_, _, idndef, _, _, _, pres, posts, body) =>
       val f = findFunction(idndef)
-      val ff = f.copy( pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = body map (_.e.inner) map exp)(f.pos, f.info, f.errT)
+      val ff = f.copy( pres = pres.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                       posts = posts.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                       body = body map (_.e.inner) map exp)(f.pos, f.info, f.errT)
       members(f.name) = ff
       ff
   }
@@ -232,7 +236,8 @@ case class Translator(program: PProgram) {
         }) getOrElse Statements.EmptyStmt)(pos, info)
       case PElse(_, els) => stmt(els)
       case PWhile(_, cond, invs, body) =>
-        While(exp(cond.inner), invs.toSeq map (inv => exp(inv.e)), stmt(body).asInstanceOf[Seqn])(pos, info)
+        While(exp(cond.inner), invs.toSeq map (inv => exp(wrapAnnotations(inv.annotations, inv.e)(inv.pos))),
+              stmt(body).asInstanceOf[Seqn])(pos, info)
       case PQuasihavoc(_, lhs, e) =>
         val (newLhs, newE) = havocStmtHelper(lhs, e)
         Quasihavoc(newLhs, newE)(pos, info)
@@ -313,6 +318,9 @@ case class Translator(program: PProgram) {
     }
   }
 
+  def wrapAnnotations(annotations: Seq[PAnnotation], pexp: PExp)(pos: (Position, Position)): PExp =
+    annotations.foldRight(pexp) { (ann, e) => new PAnnotatedExp(ann, e)(pos) }
+
   def extractAnnotation(pexp: PExp): (PExp, Map[String, Seq[String]]) = {
     pexp match {
       case PAnnotatedExp(ann, e) =>

From bc9e7475bc4d5433c3ba0673f77afd324f0824bd Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 4 Mar 2024 12:31:06 +0100
Subject: [PATCH 07/14] Fix with NoCut

---
 src/main/scala/viper/silver/parser/FastParser.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 6d93f7a29..bfc436a0f 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -827,7 +827,7 @@ class FastParser {
   // TODO does this handle positions correctly/consistently?
   // see also annotatedPrecondition, annotatedPostcondition
   def annotatedInvariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
-    P(annotation.rep(0) ~ invariant).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+    NoCut(P(annotation.rep(0) ~ invariant)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
             PSpecification[PKw.InvSpec](spec.k, spec.e, anns)(p) }.pos
 
   def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
@@ -944,7 +944,7 @@ class FastParser {
   })
 
   def annotatedPrecondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
-    P(annotation.rep(0) ~ precondition).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+    NoCut(P(annotation.rep(0) ~ precondition)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
             PSpecification[PKw.PreSpec](spec.k, spec.e, anns)(p) }.pos
 
   def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
@@ -952,7 +952,7 @@ class FastParser {
         PSpecification[PKw.PreSpec](kw, e)(p)}.pos | ParserExtension.preSpecification(ctx))
 
   def annotatedPostcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
-    P(annotation.rep(0) ~ postcondition).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+    NoCut(P(annotation.rep(0) ~ postcondition)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
       PSpecification[PKw.PostSpec](spec.k, spec.e, anns)(p) }.pos
 
   def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =

From 320c5b10f073a750e088432e98f904b4b00b15c8 Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Sun, 17 Mar 2024 22:42:38 +0100
Subject: [PATCH 08/14] Remove duplicated whitespace definition

---
 src/main/scala/viper/silver/parser/FastParser.scala | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index bfc436a0f..24abe7928 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -30,12 +30,10 @@ object FastParserCompanion {
       NoTrace((" " | "\t").rep)
   }
 
-  // TODO why is this duplicated? see FastParser below
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
       NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
-      // NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
   def identStarts[$: P] = CharIn("A-Z", "a-z", "$_")
@@ -314,16 +312,7 @@ class FastParser {
   //////////////////////////
 
   import fastparse._
-  import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym}
-
-
-  // TODO why is this duplicated? see FastParserCompanion
-  implicit val whitespace = {
-    import NoWhitespace._
-    implicit ctx: ParsingRun[_] =>
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
-      // NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
-  }
+  import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym, whitespace}
 
   implicit val lineCol: LineCol = new LineCol(this)
 

From 30cf8bb643118cb431d7f12c1fbde4a5f1ba2e9b Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Sun, 17 Mar 2024 22:49:12 +0100
Subject: [PATCH 09/14] Add positions to docAnnotations

---
 .../viper/silver/parser/FastParser.scala      | 21 +++++++------------
 1 file changed, 8 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 24abe7928..1da23d7e3 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -396,14 +396,11 @@ class FastParser {
 
   def stringLiteral[$: P]: P[PStringLiteral] = P((CharsWhile(_ != '\"').! map PRawString.apply).pos.quotes map (PStringLiteral.apply _)).pos
 
-  // TODO check positions
   def docAnnotation[$: P]: P[PAnnotation] = P("///" ~~ CharsWhile(_ != '\n', 0).!).map{
-    case s: String => p: (FilePosition, FilePosition) =>
+    case s: String => p: Pos =>
       val annotationKey = PRawString("doc")(NoPosition, NoPosition)
-      val docstring = PStringLiteral(PGrouped.apply[PSym.Quote.type, PRawString]
-                                       (PReserved.implied(PSym.Quote), PRawString(s)(NoPosition, NoPosition), PReserved.implied(PSym.Quote))
-                                                   (NoPosition, NoPosition))(NoPosition, NoPosition)
-      val annotationValues = PDelimited.implied[PStringLiteral, PSym.Comma](Seq(docstring), PReserved.implied(PSym.Comma))
+      val docstring = PStringLiteral(PGrouped[PSym.Quote.type, PRawString](PReserved.implied(PSym.Quote), PRawString(s)(p), PReserved.implied(PSym.Quote))(p))(p)
+      val annotationValues = PDelimited[PStringLiteral, PSym.Comma](Some(docstring), Seq(), None)(p)
       PAnnotation(at = PReserved.implied(PSym.At), key = annotationKey, values = PGrouped.impliedParen(annotationValues))(p)
   }.pos
 
@@ -813,14 +810,12 @@ class FastParser {
   def whileStmt[$: P]: P[PKw.While => Pos => PWhile] =
     P((parenthesizedExp ~~ semiSeparated(annotatedInvariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile(_, cond, invs, body) })
 
-  // TODO does this handle positions correctly/consistently?
-  // see also annotatedPrecondition, annotatedPostcondition
   def annotatedInvariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
-    NoCut(P(annotation.rep(0) ~ invariant)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+    NoCut(P(annotation.rep(0) ~ invariant)).map{ case (anns, spec) => p: Pos =>
             PSpecification[PKw.InvSpec](spec.k, spec.e, anns)(p) }.pos
 
   def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
-    P((P(PKw.Invariant) ~ exp).map{ case (kw, e) => p: (FilePosition, FilePosition) =>
+    P((P(PKw.Invariant) ~ exp).map{ case (kw, e) => p: Pos =>
       PSpecification[PKw.InvSpec](kw, e)(p) }.pos | ParserExtension.invSpecification(ctx))
 
   def localVars[$: P]: P[PKw.Var => Pos => PVars] =
@@ -933,7 +928,7 @@ class FastParser {
   })
 
   def annotatedPrecondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
-    NoCut(P(annotation.rep(0) ~ precondition)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+    NoCut(P(annotation.rep(0) ~ precondition)).map{ case (anns, spec) => p: Pos =>
             PSpecification[PKw.PreSpec](spec.k, spec.e, anns)(p) }.pos
 
   def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
@@ -941,11 +936,11 @@ class FastParser {
         PSpecification[PKw.PreSpec](kw, e)(p)}.pos | ParserExtension.preSpecification(ctx))
 
   def annotatedPostcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
-    NoCut(P(annotation.rep(0) ~ postcondition)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
+    NoCut(P(annotation.rep(0) ~ postcondition)).map{ case (anns, spec) => p: Pos =>
       PSpecification[PKw.PostSpec](spec.k, spec.e, anns)(p) }.pos
 
   def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
-    P((P(PKw.Ensures) ~ exp).map{ case (kw, e) => p: (FilePosition, FilePosition) =>
+    P((P(PKw.Ensures) ~ exp).map{ case (kw, e) => p: Pos =>
         PSpecification[PKw.PostSpec](kw, e)(p)}.pos | ParserExtension.postSpecification(ctx))
 
   def predicateDecl[$: P]: P[PKw.Predicate => PAnnotationsPosition => PPredicate] = P(idndef ~ argList(formalArg) ~~~ bracedExp.lw.?).map {

From 0c839f5bf0f565bf0ea8151c98aa0b1ca7939a45 Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 25 Mar 2024 08:04:15 +0100
Subject: [PATCH 10/14] Add basic test

---
 src/test/scala/DocAnnotationTests.scala | 149 ++++++++++++++++++++++++
 1 file changed, 149 insertions(+)
 create mode 100644 src/test/scala/DocAnnotationTests.scala

diff --git a/src/test/scala/DocAnnotationTests.scala b/src/test/scala/DocAnnotationTests.scala
new file mode 100644
index 000000000..16545a079
--- /dev/null
+++ b/src/test/scala/DocAnnotationTests.scala
@@ -0,0 +1,149 @@
+// 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.ast.Program
+import viper.silver.frontend._
+import viper.silver.logger.ViperStdOutLogger
+import viper.silver.reporter.StdIOReporter
+import viper.silver.parser.{PProgram, PAnnotatedExp, PWhile}
+
+class DocAnnotationTests extends AnyFunSuite {
+  object AstProvider extends ViperAstProvider(StdIOReporter(), ViperStdOutLogger("DocAnnotationTestsLogger").get) {
+    def setCode(code: String): Unit = {
+      _input = Some(code)
+    }
+
+    override def reset(input: java.nio.file.Path): Unit = {
+      if (state < DefaultStates.Initialized) sys.error("The translator has not been initialized.")
+      _state = DefaultStates.InputSet
+      _inputFile = Some(input)
+      /** must be set by [[setCode]] */
+      // _input = None
+      _errors = Seq()
+      _parsingResult = None
+      _semanticAnalysisResult = None
+      _verificationResult = None
+      _program = None
+      resetMessages()
+    }
+  }
+
+  def generatePAstAndAst(code: String): Option[(PProgram, Program)] = {
+    val code_id = code.hashCode.asInstanceOf[Short].toString
+    AstProvider.setCode(code)
+    AstProvider.execute(Seq("--ignoreFile", code_id))
+
+    if (AstProvider.errors.isEmpty) {
+      Some(AstProvider.parsingResult, AstProvider.translationResult)
+    } else {
+      AstProvider.logger.error(s"An error occurred while translating ${AstProvider.errors}")
+      None
+    }
+  }
+
+  test("Basic parsing of documentation") {
+    import viper.silver.ast._
+
+    val code =
+      """/// a field
+        |field f: Int
+        |/// P is a predicate
+        |predicate P(x: Int)
+        |
+        |/// a function
+        |function fun(x: Int): Int {
+        |  (x / 1 == x) ? 42 : 0
+        |}
+        |/// a second function
+        |function fun2(x: Int): Int
+        |    /// precondition
+        |    requires x > 0
+        |    /// post-
+        |    /// condition
+        |    ensures result > 0
+        |
+        |/// very important domain
+        |domain ImportantType {
+        |
+        |  /// this function
+        |  /// is crucial
+        |  function phi(ImportantType): Int
+        |
+        |  /// the only axiom
+        |  axiom {
+        |    /// documenting an expression
+        |    true
+        |  }
+        |}
+        |
+        |/// a macro
+        |define plus(a, b) (a+b)
+        |
+        |/// this is a method
+        |/// it does something
+        |method m(x: Ref, y: Ref)
+        |    /// this documents the first precondition
+        |    requires acc(x.f)
+        |    /// documentation of the second precondition
+        |    requires acc(y.f)
+        |{
+        |    var local: Bool
+        |
+        |    while (true)///the invariant
+        |      /// is always true
+        |      invariant true
+        |      /// termination
+        |      decreases x.f
+        |    {}
+        |
+        |}
+        |""".stripMargin
+
+    val pAst: PProgram = generatePAstAndAst(code).get._1
+
+    val fieldAnn = pAst.fields.head.annotations.head.values.inner.first.get.str
+    assert(fieldAnn == " a field")
+
+    val predicateAnnotation = pAst.predicates.head.annotations.head.values.inner.first.get.str
+    assert(predicateAnnotation == " P is a predicate")
+
+    val functionAnnotation = pAst.functions.head.annotations.head.values.inner.first.get.str
+    assert(functionAnnotation == " a function")
+
+    val fun2Annotation = pAst.functions(1).annotations.head.values.inner.first.get.str
+    val fun2PreAnnotations = pAst.functions(1).pres.head.annotations.map(_.values.inner.first.get.str)
+    val fun2PostAnnotations = pAst.functions(1).posts.head.annotations.map(_.values.inner.first.get.str)
+    assert(fun2Annotation == " a second function")
+    assert(fun2PreAnnotations == Seq(" precondition"))
+    assert(fun2PostAnnotations == Seq(" post-", " condition"))
+
+    val domainAnnotation = pAst.domains.head.annotations.head.values.inner.first.get.str
+    assert(domainAnnotation == " very important domain")
+
+    val domainFunctionAnnotations = pAst.domains.head.members.inner.funcs.head.annotations.map(_.values.inner.first.get.str)
+    assert(domainFunctionAnnotations == Seq(" this function", " is crucial"))
+
+    val axiomAnnotations = pAst.domains.head.members.inner.axioms.head.annotations.map(_.values.inner.first.get.str)
+    assert(axiomAnnotations == Seq(" the only axiom"))
+    val axiomExpAnnotations = pAst.domains.head.members.inner.axioms.head.exp.e.inner.asInstanceOf[PAnnotatedExp].annotation.values.inner.first.get.str
+    assert(axiomExpAnnotations == " documenting an expression")
+
+    val macroAnnotation = pAst.macros.head.annotations.head.values.inner.first.get.str
+    assert(macroAnnotation == " a macro")
+
+    val methodAnnotations = pAst.methods.head.annotations.map(_.values.inner.first.get.str)
+    assert(methodAnnotations == Seq(" this is a method", " it does something"))
+
+    val methodPreAnnotations = pAst.methods.head.pres.toSeq.map(_.annotations.head.values.inner.first.get.str)
+    assert(methodPreAnnotations == Seq(" this documents the first precondition", " documentation of the second precondition"))
+
+    val loopInvariantAnnotations = pAst.methods.head.body.get.ss.inner.inner.collect {
+          case (_, w: PWhile) => w.invs.toSeq.flatMap(_.annotations.map(_.values.inner.first.get.str))
+    }.flatten
+    assert(loopInvariantAnnotations == Seq("the invariant", " is always true", " termination"))
+  }
+}
\ No newline at end of file

From 9c7b16f4518337a0640cca1e9ca82ea03cbf004c Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Mon, 25 Mar 2024 11:32:27 +0100
Subject: [PATCH 11/14] Only parse exactly three slashes as beginning of
 documentation

---
 src/main/scala/viper/silver/parser/FastParser.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 1da23d7e3..75a9fa8e2 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -33,7 +33,7 @@ object FastParserCompanion {
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ !StringIn("/") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      NoTrace((("/*" ~ (!"*/" ~ AnyChar).rep ~ "*/") | ((("//" ~ !("/")) | "////") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
   def identStarts[$: P] = CharIn("A-Z", "a-z", "$_")

From ee33a3618610a92b3cc581f04534fd1cba9e241c Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Tue, 21 May 2024 13:08:56 +0200
Subject: [PATCH 12/14] Implement feedback wip

---
 .../viper/silver/parser/FastParser.scala      | 12 ++---
 .../scala/viper/silver/parser/ParseAst.scala  |  7 ++-
 .../viper/silver/parser/ParseAstKeyword.scala |  3 ++
 .../viper/silver/parser/Translator.scala      | 52 +++++++++++++++----
 4 files changed, 54 insertions(+), 20 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 75a9fa8e2..09d03f619 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -396,15 +396,11 @@ class FastParser {
 
   def stringLiteral[$: P]: P[PStringLiteral] = P((CharsWhile(_ != '\"').! map PRawString.apply).pos.quotes map (PStringLiteral.apply _)).pos
 
-  def docAnnotation[$: P]: P[PAnnotation] = P("///" ~~ CharsWhile(_ != '\n', 0).!).map{
-    case s: String => p: Pos =>
-      val annotationKey = PRawString("doc")(NoPosition, NoPosition)
-      val docstring = PStringLiteral(PGrouped[PSym.Quote.type, PRawString](PReserved.implied(PSym.Quote), PRawString(s)(p), PReserved.implied(PSym.Quote))(p))(p)
-      val annotationValues = PDelimited[PStringLiteral, PSym.Comma](Some(docstring), Seq(), None)(p)
-      PAnnotation(at = PReserved.implied(PSym.At), key = annotationKey, values = PGrouped.impliedParen(annotationValues))(p)
-  }.pos
+  def docString[$: P]: P[PRawString] = P(CharsWhile(_ != '\n', 0).! map PRawString.apply).pos
+
+  def docAnnotation[$: P]: P[PAnnotation] = P(P(PSym.TripleSlash) ~~ docString).map{ case (s, d) => p => PDocAnnotation(s, d)(p) }.pos
 
-  def annotation[$: P]: P[PAnnotation] = P(P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos | docAnnotation)
+  def annotation[$: P]: P[PAnnotation] = P(P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAtAnnotation.apply _).tupled).pos | docAnnotation)
 
   def annotated[$: P, T](inner: => P[PAnnotationsPosition => T]): P[T] = P((annotation.rep(0) ~ inner).map {
     case (annotations, i) => pos: Pos => i(PAnnotationsPosition(annotations, pos))
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 920b98246..d4fc8a349 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1694,10 +1694,15 @@ case class PMethodReturns(k: PKw.Returns, formalReturns: PGrouped.Paren[PDelimit
   */
 case class PAnnotationsPosition(annotations: Seq[PAnnotation], pos: (FilePosition, FilePosition))
 
-case class PAnnotation(at: PSym.At, key: PRawString, values: PGrouped.Paren[PDelimited[PStringLiteral, PSym.Comma]])(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
+sealed trait PAnnotation extends PNode with PPrettySubnodes {
+  def key: PRawString
   override def pretty: String = super.pretty + "\n"
 }
 
+case class PAtAnnotation(at: PSym.At, key: PRawString, values: PGrouped.Paren[PDelimited[PStringLiteral, PSym.Comma]])(val pos: (Position, Position)) extends PNode with PAnnotation with PPrettySubnodes {}
+
+case class PDocAnnotation(tripleSlash: PSym.TripleSlash, docString: PRawString, key: PRawString = PRawString("doc")(NoPosition, NoPosition))(val pos: (Position, Position)) extends PAnnotation {}
+
 // Any unenclosed string (e.g. `hello`)
 case class PRawString(str: String)(val pos: (Position, Position)) extends PNode with PLeaf {
   override def display: String = str
diff --git a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
index 646c14819..78a3bc2a1 100644
--- a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
+++ b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
@@ -321,6 +321,9 @@ object PSym {
   // Used for annotations
   case object At extends PSym("@") with PSymbolLang
   type At = PReserved[At.type]
+  // Used for documentation
+  case object TripleSlash extends PSym("///") with PSymbolLang
+  type TripleSlash = PReserved[TripleSlash.type]
   // Used for `new(*)`
   case object Star extends PSym("*") with PSymbolLang
   type Star = PReserved[Star.type]
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 3d131c38e..8f99805f7 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -325,12 +325,26 @@ case class Translator(program: PProgram) {
     pexp match {
       case PAnnotatedExp(ann, e) =>
         val (resPexp, innerMap) = extractAnnotation(e)
-        val combinedValue = if (innerMap.contains(ann.key.str)) {
-          ann.values.inner.toSeq.map(_.str) ++ innerMap(ann.key.str)
-        } else {
-          ann.values.inner.toSeq.map(_.str)
+        val key = ann match {
+          case ann: PAtAnnotation => ann.key.str
+          case ann: PDocAnnotation => "doc"
         }
-        (resPexp, innerMap.updated(ann.key.str, combinedValue))
+        val combinedValue =
+          ann match {
+            case ann: PAtAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.values.inner.toSeq.map(_.str) ++ innerMap(key)
+              } else {
+                ann.values.inner.toSeq.map(_.str)
+              }
+            case ann: PDocAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.docString.str +: innerMap(key)
+              } else {
+                Seq(ann.docString.str)
+              }
+          }
+        (resPexp, innerMap.updated(key, combinedValue))
       case _ => (pexp, Map())
     }
   }
@@ -339,12 +353,26 @@ case class Translator(program: PProgram) {
     pStmt match {
       case PAnnotatedStmt(ann, s) =>
         val (resPStmt, innerMap) = extractAnnotationFromStmt(s)
-        val combinedValue = if (innerMap.contains(ann.key.str)) {
-          ann.values.inner.toSeq.map(_.str) ++ innerMap(ann.key.str)
-        } else {
-          ann.values.inner.toSeq.map(_.str)
+        val key = ann match {
+          case ann: PAtAnnotation => ann.key.str
+          case ann: PDocAnnotation => "doc"
         }
-        (resPStmt, innerMap.updated(ann.key.str, combinedValue))
+        val combinedValue =
+          ann match {
+            case ann: PAtAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.values.inner.toSeq.map(_.str) ++ innerMap(key)
+              } else {
+                ann.values.inner.toSeq.map(_.str)
+              }
+            case ann: PDocAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.docString.str +: innerMap(key)
+              } else {
+                Seq(ann.docString.str)
+              }
+          }
+        (resPStmt, innerMap.updated(key, combinedValue))
       case _ => (pStmt, Map())
     }
   }
@@ -731,7 +759,9 @@ object Translator {
     if (annotations.isEmpty) {
       NoInfo
     } else {
-      AnnotationInfo(annotations.groupBy(_.key).map{ case (k, v) => k.str -> v.flatMap(_.values.inner.toSeq.map(_.str)) })
+      AnnotationInfo(annotations.groupBy(_.key).map{ case (k, v) => k.str -> v.flatMap{
+                         case a: PAtAnnotation => a.values.inner.toSeq.map(_.str)
+                         case a: PDocAnnotation => Seq(a.docString.str) }})
     }
   }
 }

From b2d0d9f862b6e43457aa118e003997ef5ed3e548 Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Tue, 13 Aug 2024 23:31:22 +0200
Subject: [PATCH 13/14] Add DocPlugin to extract sparser documentation tree
 from CST

This is used as input for the website generation frontend.
---
 .../plugin/standard/doc/DocPlugin.scala       | 138 ++++++++++++++++++
 1 file changed, 138 insertions(+)
 create mode 100644 src/main/scala/viper/silver/plugin/standard/doc/DocPlugin.scala

diff --git a/src/main/scala/viper/silver/plugin/standard/doc/DocPlugin.scala b/src/main/scala/viper/silver/plugin/standard/doc/DocPlugin.scala
new file mode 100644
index 000000000..e2b095e6c
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/doc/DocPlugin.scala
@@ -0,0 +1,138 @@
+// 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-2019 ETH Zurich.
+
+package viper.silver.plugin.standard.doc
+
+import viper.silver.plugin.SilverPlugin
+import viper.silver.ast.{Program, FilePosition, NoPosition, Position}
+import viper.silver.parser.{PProgram, PFieldDecl, PFields, PNode, PAnnotated, PAnnotatedExp,
+  PAnnotatedStmt, PAnnotation, PAtAnnotation, PDocAnnotation, PMethod, PFunction, PStringLiteral,
+  PAxiom, PSpecification, PRawString, PIdnRef, PPredicate, PDomain, PDomainFunction, Translator}
+import viper.silver.ast.utility.Visitor
+import upickle.default._
+import java.io._
+import viper.silver.frontend.SilFrontend
+import viper.silver.verifier.ParseReport
+
+case class DocReport(message: String, override val pos: Position)
+  extends ParseReport(message, pos) {
+  def fullId = "parser.documentation"
+  def readableMessage = message
+}
+
+class DocPlugin extends SilverPlugin {
+
+  case class DocNode(nodeType: String, info: NodeInfo, pos: (String, String), doc: String = "", children: Seq[DocNode]) {
+    /** @see [[Visitor.reduceTree()]] */
+    def reduceTree[T](f: (DocNode, Seq[T]) => T) = Visitor.reduceTree(this, DocNode.callSubnodes)(f)
+
+    /** @see [[Visitor.reduceWithContext()]] */
+    def reduceWithContext[C, R](context: C, enter: (DocNode, C) => C, combine: (DocNode, C, Seq[R]) => R) = {
+      Visitor.reduceWithContext(this, DocNode.callSubnodes)(context, enter, combine)
+    }
+  }
+
+  object DocNode {
+    def callSubnodes(n: DocNode): Seq[DocNode] = n.children
+    implicit lazy val rw: ReadWriter[DocNode] = macroRW
+  }
+
+  case class VarInfo(name: String, typ: String)
+  case class NodeInfo(name: String = "", typ: String = "",
+                      args: Seq[VarInfo] = Seq(),
+                      returns: Seq[VarInfo] = Seq(),
+                      misc: String = "")
+
+  object VarInfo {
+    implicit lazy val rw: ReadWriter[VarInfo] = macroRW
+  }
+  object NodeInfo {
+    implicit lazy val rw: ReadWriter[NodeInfo] = macroRW
+  }
+
+  /** Called after identifiers have been resolved but before the parse AST is
+    * translated into the normal AST.
+    *
+    * @param input
+    *   Parse AST
+    * @return
+    *   Modified Parse AST
+      */
+  override def beforeTranslate(input: PProgram): PProgram = {
+    val extractInfo: PNode => NodeInfo = {
+      // case n: PFields => Map("name" -> n.toString())
+      case PIdnRef(name) => NodeInfo(name)
+      case PFieldDecl(idndef, colon, typ) => NodeInfo(idndef.name, typ.toString())
+      case n: PMethod =>
+        NodeInfo(n.idndef.name, "", n.args.inner.toSeq.map(a => VarInfo(a.idndef.name, a.typ.toString())),
+                 n.returns match {
+                   case Some(returns) => returns.formalReturns.inner.toSeq.map(a => VarInfo(a.idndef.name, a.typ.toString()))
+                   case None => Seq() })
+      case n: PFunction =>
+        NodeInfo(n.idndef.name, n.resultType.toString(),
+                 n.args.inner.toSeq.map(a => VarInfo(a.idndef.name, a.typ.toString())))
+      case n: PPredicate => NodeInfo(n.idndef.name, "", n.args.inner.toSeq.map(a => VarInfo(a.idndef.name, a.typ.toString())))
+      case n: PDomain =>
+        NodeInfo(n.idndef.name, "",
+                 n.typVars match {
+                   case Some(typVars) => typVars.inner.toSeq.map(a => VarInfo("", a.idndef.name))
+                   case None => Seq() })
+      case n: PDomainFunction =>
+        NodeInfo(n.idndef.name, n.resultType.toString(),
+                 n.args.inner.toSeq.map(a =>
+                   VarInfo(a.name match {case Some(idndef) => idndef.name case None => ""}, a.typ.toString())),
+                 Seq(), n.unique match {case Some(kw) => kw.display.trim() case None => ""})
+      case n: PAxiom =>
+        NodeInfo(n.idndef match {case Some(id) => id.name case None => ""})
+      case n: PSpecification[_] => NodeInfo(n.k.rs.display.trim())
+      case _ => NodeInfo()
+    }
+
+    val extractPos: PNode => (String, String) = n => (n.pos._1.toString(), n.pos._2.toString())
+
+    val collectDocs: Seq[PAnnotation] => String = _.collect{ case k: PAtAnnotation if (k.key.str == "doc") => k.values.inner.toSeq.map(_.str)
+      case k: PDocAnnotation => Seq(k.docString.str) }.flatten.mkString("\n")
+    val translator: Translator = new Translator(input);
+    val extractDoc: PNode => String =
+      ({
+         case e: PAnnotatedExp => translator.extractAnnotation(e)._2.getOrElse("doc", Seq()).mkString("\n")
+         case s: PAnnotatedStmt => translator.extractAnnotationFromStmt(s)._2.getOrElse("doc", Seq()).mkString("\n")
+         case n: PAnnotated => collectDocs(n.annotations)
+         case n: PSpecification[_] => collectDocs(n.annotations)
+         case n: PAxiom => collectDocs(n.annotations)
+         case _ => ""
+       }: PNode => String)
+
+    val removeRoots: Seq[DocNode] => Seq[DocNode] = s => s.flatMap{
+      case t: DocNode if (t.nodeType == "*root*") => t.children
+      case n: DocNode => Seq(n)
+    }
+
+    val docTree = input.reduceTree(
+      (n: PNode, children: Seq[DocNode]) => {
+        val createDocNode = ((kind: String, n: PNode) =>
+          DocNode(kind, extractInfo(n), extractPos(n), extractDoc(n), removeRoots(children)))
+
+        n match {
+          case n: PIdnRef[_]                 => createDocNode("IdnRef", n)
+          case n: PFieldDecl                 => createDocNode("FieldDecl", n)
+          case n: PMethod                    => createDocNode("Method", n)
+          case n: PFunction                  => createDocNode("Function", n)
+          case n: PSpecification[_]          => createDocNode("Specification", n)
+          case n: PPredicate                 => createDocNode("Predicate", n)
+          case n: PDomain                    => createDocNode("Domain", n)
+          case n: PAxiom                     => createDocNode("Axiom", n)
+          case n: PDomainFunction            => createDocNode("DomainFunction", n)
+          case _                             => DocNode("*root*", NodeInfo(), ("", ""), "", removeRoots(children))
+        }
+      })
+
+    val json: String = write(docTree)
+    println(json)
+
+    PProgram(input.imported, input.members)(input.pos, DocReport(json, NoPosition) +: input.localErrors)
+  }
+}

From 125aa7c197760706103e6cae8deb686e8f793427 Mon Sep 17 00:00:00 2001
From: fnussbaum <ferdinand.nussbaum@inf.ethz.ch>
Date: Tue, 13 Aug 2024 23:32:47 +0200
Subject: [PATCH 14/14] Add command line entry point similar to silicon

---
 silver.sh                                     | 13 +++++++++
 .../scala/viper/silver/SilverRunner.scala     | 28 +++++++++++++++++++
 2 files changed, 41 insertions(+)
 create mode 100755 silver.sh
 create mode 100644 src/main/scala/viper/silver/SilverRunner.scala

diff --git a/silver.sh b/silver.sh
new file mode 100755
index 000000000..383464af0
--- /dev/null
+++ b/silver.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+set -e
+
+BASEDIR="$(realpath "$(dirname "$0")")"
+
+CP_FILE="$BASEDIR/silver_classpath.txt"
+
+if [ ! -f "$CP_FILE" ]; then
+    (cd "$BASEDIR"; sbt "export runtime:dependencyClasspath" | tail -n1 > "$CP_FILE")
+fi
+
+exec java -cp "$(cat "$CP_FILE")" viper.silver.SilverRunner "$@"
diff --git a/src/main/scala/viper/silver/SilverRunner.scala b/src/main/scala/viper/silver/SilverRunner.scala
new file mode 100644
index 000000000..0aaa8188b
--- /dev/null
+++ b/src/main/scala/viper/silver/SilverRunner.scala
@@ -0,0 +1,28 @@
+package viper.silver
+
+
+import scala.collection.immutable.ArraySeq
+import viper.silver.frontend.DefaultStates 
+import viper.silver.frontend.ViperAstProvider
+import viper.silver.logger.SilentLogger
+import viper.silver.reporter.NoopReporter
+
+
+object SilverRunner extends SilverRunnerInstance {
+  def main(args: Array[String]): Unit = {
+    runMain(args)
+  }
+}
+
+class SilverRunnerInstance extends ViperAstProvider(NoopReporter, SilentLogger().get) {
+  def runMain(args: Array[String]): Unit = {
+    var exitCode = 1 /* Only 0 indicates no error */
+
+    execute(ArraySeq.unsafeWrapArray(args))
+    
+    if (state >= DefaultStates.Translation) {
+      exitCode = 0
+    }
+    sys.exit(exitCode)
+  }
+}
\ No newline at end of file