Skip to content

Commit 5a906ae

Browse files
committed
Fix with NoCut
1 parent 38dcf16 commit 5a906ae

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -827,7 +827,7 @@ class FastParser {
827827
// TODO does this handle positions correctly/consistently?
828828
// see also annotatedPrecondition, annotatedPostcondition
829829
def annotatedInvariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
830-
P(annotation.rep(0) ~ invariant).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
830+
NoCut(P(annotation.rep(0) ~ invariant)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
831831
PSpecification[PKw.InvSpec](spec.k, spec.e, anns)(p) }.pos
832832

833833
def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
@@ -944,15 +944,15 @@ class FastParser {
944944
})
945945

946946
def annotatedPrecondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
947-
P(annotation.rep(0) ~ precondition).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
947+
NoCut(P(annotation.rep(0) ~ precondition)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
948948
PSpecification[PKw.PreSpec](spec.k, spec.e, anns)(p) }.pos
949949

950950
def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
951951
P((P(PKw.Requires) ~ exp).map{ case (kw, e) => p: (FilePosition, FilePosition) =>
952952
PSpecification[PKw.PreSpec](kw, e)(p)}.pos | ParserExtension.preSpecification(ctx))
953953

954954
def annotatedPostcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
955-
P(annotation.rep(0) ~ postcondition).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
955+
NoCut(P(annotation.rep(0) ~ postcondition)).map{ case (anns, spec) => p: (FilePosition, FilePosition) =>
956956
PSpecification[PKw.PostSpec](spec.k, spec.e, anns)(p) }.pos
957957

958958
def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =

0 commit comments

Comments
 (0)