Fix with NoCut

viperproject · Mar 18, 2024 · 5a906ae · 5a906ae
1 parent 38dcf16
commit 5a906ae
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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,15 +944,15 @@ 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]] =
     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.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]] =