Allowing . in annotation keys

Author: marcoeilers

src/main/scala/viper/silver/parser/FastParser.scala

@@ -805,7 +805,7 @@ class FastParser {
 
   def stringLiteral[$: P]: P[String] = P("\"" ~ CharsWhile(_ != '\"').! ~ "\"")
 
-  def annotation[$: P]: P[(String, Seq[String])] = P("@" ~~ ident ~ parens(stringLiteral.rep(sep = ",")))
+  def annotation[$: P]: P[(String, Seq[String])] = P("@" ~~ annotationIdentifier ~ parens(stringLiteral.rep(sep = ",")))
 
   def annotatedAtom[$: P]: P[PExp] = FP(annotation ~ atom).map{
     case (pos, (key, value, exp)) => PAnnotatedExp(exp, (key, value))(pos)
@@ -827,6 +827,8 @@ class FastParser {
 
   def identifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX
 
+  def annotationIdentifier[$: P]: P[String] = (CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!
+
   def ident[$: P]: P[String] = identifier.!.filter(a => !keywords.contains(a)).opaque("invalid identifier (could be a keyword)")
 
   def idnuse[$: P]: P[PIdnUse] = FP(ident).map { case (pos, id) => PIdnUse(id)(pos) }

src/test/resources/all/annotation/annotationSuccess.vpr

@@ -35,7 +35,7 @@ method m(x: Ref, y: Ref)
     requires acc(y.f)
 {
     var tmp: Int
-    @annotatingastatement("the assignment")
+    @annotating.a.statement("the assignment")
     tmp := @asd("test 123") fun02(x, @ann("this is ugly") y, true)
     y.f := 1
     assert tmp == fun02(x, y, true)

src/test/scala/AstAnnotationTests.scala

@@ -88,7 +88,7 @@ class AstAnnotationTests extends AnyFunSuite {
         |    var tmp: Int
         |    @annotatingastatement("the assignment", "12")
         |    @annotatingastatement("34")
-        |    @suchannotations()
+        |    @such.annotations()
         |    tmp := @asd("test 123") fun02(x, @ann("this is ugly") y, true)
         |    y.f := 1
         |    assert tmp == fun02(x, y, true)
@@ -108,7 +108,7 @@ class AstAnnotationTests extends AnyFunSuite {
 
     val assignment = res.methods.head.body.get.ss(1)
     val assignmentAnn = assignment.info.getUniqueInfo[AnnotationInfo].get
-    assert(assignmentAnn.values == Map("annotatingastatement" -> Seq("the assignment", "12", "34"), "suchannotations" -> Seq()))
+    assert(assignmentAnn.values == Map("annotatingastatement" -> Seq("the assignment", "12", "34"), "such.annotations" -> Seq()))
 
     val rhs = assignment.asInstanceOf[LocalVarAssign].rhs
     val rhsAnn = rhs.info.getUniqueInfo[AnnotationInfo].get