Merge pull request #793 from viperproject/meilers_fix_787

Fixing macro substitution for label statements

Author: marcoeilers

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

@@ -481,6 +481,19 @@ object MacroExpander {
           freeVars += varUse.name
           (varUse, ctx)
         }
+      case (label@PLabel(lbl, lName, invs), ctx) if !ctx.c.boundVars.contains(lName.name) =>
+        if (ctx.c.paramToArgMap.contains(lName.name)) {
+          val replacement = ctx.c.paramToArgMap(lName.name).deepCopyAll
+          val replaced = replacement match {
+            case r: PIdnUseExp => PIdnDef(r.name)(r.pos)
+            case r =>
+              throw MacroException(s"macro expansion cannot substitute expression `${replacement.pretty}` at ${replacement.pos._1} in non-expression position at ${lName.pos._1}.", replacement.pos)
+          }
+          (PLabel(lbl, replaced, invs)(label.pos), ctx.updateContext(ctx.c.copy(paramToArgMap = ctx.c.paramToArgMap.empty)))
+        } else {
+          freeVars += lName.name
+          (label, ctx)
+        }
     }, ReplaceContext())
     (replacer, freeVars)
   }

src/test/resources/all/issues/silver/0787a.vpr

@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method main()
+{
+    m(some_name)
+}
+
+define m(label_name)
+{
+    goto label_name
+    label label_name
+}

src/test/resources/all/issues/silver/0787b.vpr

@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method main()
+{
+    //:: ExpectedOutput(parser.error)
+    m(3)
+}
+
+define m(label_name)
+{
+    label label_name
+}