Fix for dotted attribute names in outer parser (#3953)

We serialize Java objects directly to represent the source and location attributes in `compiled.txt`; this breaks the part of the outer parser responsible for lexing an identifier name (#3952). To avoid having to rewrite every bit of code that deals with these attributes, we instead just make the lexical specification of attribute names a bit more relaxed. Fixes #3952 Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Feb 5, 2024 · 7734da1 · 7734da1
1 parent 3fee0eb
commit 7734da1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/kernel/src/main/javacc/Outer.jj b/kernel/src/main/javacc/Outer.jj
@@ -645,7 +645,7 @@ List<Tag> KLabels() :
 | "]" { matchedToken.kind = RSQUARE; }
 | "(" { matchedToken.kind = LPAREN; }
 | ")" { matchedToken.kind = RPAREN; }
-| <KEY: ["a"-"z","1"-"9"](["A"-"Z", "a"-"z", "-", "0"-"9"])*("<" (["A"-"Z", "a"-"z", "-", "0"-"9"])+ ">")?>
+| <KEY: ["a"-"z","1"-"9"](["A"-"Z", "a"-"z", "-", "0"-"9", "."])*("<" (["A"-"Z", "a"-"z", "-", "0"-"9"])+ ">")?>
 }
 
 /** The same as 'Attributes()', but requires that the entire input be