Merge pull request #795 from viperproject/meilers_disallow_nested_macros

Add argument to properly disallow nested macros

Author: marcoeilers

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

@@ -751,7 +751,7 @@ class FastParser {
   }
 
   def stmt(allowDefine: Boolean = true)(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | annotatedStmt |
-    stmtReservedKw(allowDefine) | stmtBlock() |
+    stmtReservedKw(allowDefine) | stmtBlock(allowDefine) |
     assign | ParserExtension.newStmtAtEnd(ctx))
 
   def annotatedStmt(implicit ctx : P[_]): P[PStmt] = P((annotation ~ stmt()) map (PAnnotatedStmt.apply _).tupled).pos

src/test/resources/all/issues/silver/0786.vpr

@@ -0,0 +1,12 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+define outer_macro () {
+  //:: ExpectedOutput(parser.error)
+  { define inner_macro 42 }
+}
+
+method test()
+{
+  outer_macro()
+}