Skip to content

Commit 348c2a5

Browse files
committed
Fix a small issue with statement macros
1 parent b4ed514 commit 348c2a5

4 files changed

Lines changed: 12 additions & 27 deletions

File tree

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -596,7 +596,7 @@ class FastParser {
596596

597597
val matchOnMacroCall: PartialFunction[PNode, MacroApp] = {
598598
case app: PMacroRef => MacroApp(app.idnuse.name, Nil, app)
599-
case app: PMethodCall if isMacro(app.method.name) => MacroApp(app.method.name, app.args, app)
599+
case app@PAssign(_, call: PCall) if isMacro(call.func.name) => MacroApp(call.func.name, call.args, app)
600600
case app: PCall if isMacro(app.func.name) => MacroApp(app.func.name, app.args, app)
601601
case app: PIdnUse if isMacro(app.name) => MacroApp(app.name, Nil, app)
602602
}
@@ -766,7 +766,8 @@ class FastParser {
766766
}
767767
case target => target
768768
}
769-
(PAssign(expandedTargets, rhs)(assign.pos), ctx)
769+
val expandedLhs = PAssign(expandedTargets, rhs)(assign.pos)
770+
(ExpandMacroIfValid(expandedLhs, ctx), ctx)
770771

771772
// Handles all other calls to macros
772773
case (node, ctx) => (ExpandMacroIfValid(node, ctx), ctx)
@@ -778,7 +779,6 @@ class FastParser {
778779
* Recursing into such PIdnUse nodes caused Silver issue #205.
779780
*/
780781
case PMacroRef(_) => Seq.empty
781-
case PMethodCall(targets, _, args) => Seq(targets, args)
782782
case PCall(_, args, typeAnnotated) => Seq(args, typeAnnotated)
783783
}.repeat
784784

@@ -1090,7 +1090,7 @@ class FastParser {
10901090

10911091
def newExp[$: P]: P[PNewExp] = FP("new" ~ "(" ~ newExpFields ~ ")").map { case (pos, fields) => PNewExp(fields)(pos) }
10921092

1093-
def newExpFields[$: P]: P[Option[Seq[PIdnUse]]] = P(idnuse.rep(sep = ",")).map(Some(_)) | P("*").map(_ => None)
1093+
def newExpFields[$: P]: P[Option[Seq[PIdnUse]]] = P(P("*").map(_ => None) | P(idnuse.rep(sep = ",")).map(Some(_)))
10941094

10951095
def fapp[$: P]: P[PCall] = FP(idnuse ~ parens(actualArgList)).map {
10961096
case (pos, (func, args)) =>
@@ -1113,7 +1113,7 @@ class FastParser {
11131113

11141114
def macroref[$: P]: P[PMacroRef] = FP(idnuse).map { case (pos, a) => PMacroRef(a)(pos) }
11151115

1116-
def assignTarget[$: P]: P[PAssignTarget] = fieldAcc | NoCut(fapp) | idnuse
1116+
def assignTarget[$: P]: P[PAssignTarget] = P(fieldAcc | NoCut(fapp) | idnuse)
11171117

11181118
def assign[$: P]: P[PAssign] = FP((assignTarget.rep(min = 1, sep = ",") ~ ":=").? ~ exp).map { case (pos, (targets, rhs)) => PAssign(targets.getOrElse(Seq()), rhs)(pos) }
11191119

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1234,8 +1234,6 @@ case class PLocalVarDecl(vars: Seq[PFormalArgDecl], init: Option[PAssign])(val p
12341234

12351235
case class PGlobalVarDecl(idndef: PIdnDef, typ: PType)(val pos: (Position, Position)) extends PTypedDeclaration with PUniversalDeclaration
12361236

1237-
case class PMethodCall(targets: Seq[PIdnUse], method: PIdnUse, args: Seq[PExp])(val pos: (Position, Position)) extends PStmt
1238-
12391237
case class PLabel(idndef: PIdnDef, invs: Seq[PExp])(val pos: (Position, Position)) extends PStmt with PLocalDeclaration
12401238

12411239
case class PGoto(targets: PIdnUse)(val pos: (Position, Position)) extends PStmt
@@ -1485,7 +1483,6 @@ object Nodes {
14851483
case PInhale(exp) => Seq(exp)
14861484
case PAssume(exp) => Seq(exp)
14871485
case PNewExp(fields) => fields.getOrElse(Seq())
1488-
case PMethodCall(targets, method, args) => targets ++ Seq(method) ++ args
14891486
case PLabel(name, invs) => Seq(name) ++ invs
14901487
case PGoto(label) => Seq(label)
14911488
case PAssign(targets, rhs) => targets ++ Seq(rhs)

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,6 @@ object Transformer {
136136
case p@PIf(cond, thn, els) => PIf(go(cond), go(thn), go(els))(p.pos)
137137
case p@PWhile(cond, invs, body) => PWhile(go(cond), invs map go, go(body))(p.pos)
138138
case p@PLocalVarDecl(vars, init) => PLocalVarDecl(vars map go, init map go)(p.pos)
139-
case p@PMethodCall(targets, method, args) => PMethodCall(targets map go, go(method), args map go)(p.pos)
140139
case p@PLabel(idndef, invs) => PLabel(go(idndef), invs map go)(p.pos)
141140
case p@PGoto(target) => PGoto(go(target))(p.pos)
142141
case p@PDefine(idndef, optArgs, exp) => PDefine(go(idndef), optArgs map (_ map go) , go(exp))(p.pos)

src/main/scala/viper/silver/verifier/VerificationError.scala

Lines changed: 7 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -273,27 +273,16 @@ object errors {
273273
def Internal(offendingNode: ErrorNode = DummyNode): PartialVerificationError =
274274
PartialVerificationError((reason: ErrorReason) => Internal(offendingNode, reason))
275275

276-
case class AssignmentTargetFailed(offendingNode: Lhs, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
277-
val id = "assignment.target.failed"
278-
val text = "Assignment target might fail."
276+
case class AssignmentFailed(offendingNode: Stmt, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
277+
val id = "assignment.failed"
278+
val text = "Assignment might fail."
279279

280-
def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = AssignmentTargetFailed(offendingNode.asInstanceOf[Lhs], this.reason, this.cached)
281-
def withReason(r: ErrorReason) = AssignmentTargetFailed(offendingNode, r, cached)
280+
def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = AssignmentFailed(offendingNode.asInstanceOf[Stmt], this.reason, this.cached)
281+
def withReason(r: ErrorReason) = AssignmentFailed(offendingNode, r, cached)
282282
}
283283

284-
def AssignmentTargetFailed(offendingNode: Lhs): PartialVerificationError =
285-
PartialVerificationError((reason: ErrorReason) => AssignmentTargetFailed(offendingNode, reason))
286-
287-
case class AssignmentValueFailed(offendingNode: Exp, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
288-
val id = "assignment.value.failed"
289-
val text = "Assignment value might fail."
290-
291-
def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = AssignmentValueFailed(offendingNode.asInstanceOf[Exp], this.reason, this.cached)
292-
def withReason(r: ErrorReason) = AssignmentValueFailed(offendingNode, r, cached)
293-
}
294-
295-
def AssignmentValueFailed(offendingNode: Exp): PartialVerificationError =
296-
PartialVerificationError((reason: ErrorReason) => AssignmentValueFailed(offendingNode, reason))
284+
def AssignmentFailed(offendingNode: Stmt): PartialVerificationError =
285+
PartialVerificationError((reason: ErrorReason) => AssignmentFailed(offendingNode, reason))
297286

298287
case class CallFailed(offendingNode: MethodCall, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
299288
val id = "call.failed"

0 commit comments

Comments
 (0)