viperproject / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
78 stars 40 forks source link

Syntax crash when defining a statement macro inside another statement macro #786

Closed Bibin112358 closed 3 months ago

Bibin112358 commented 4 months ago

Viper-Extension tells me to report this bug:

Using the following Viper Program

define outer_macro () {
  { define inner_macro 42 }
}

method test()
{
  outer_macro()
}

I get the error message:

Constructing the AST has failed: internal error during typechecking. Please file a bug report at https://github.com/viperproject/silver. Error "java.lang.RuntimeException: Unexpected node PDefine(List(),PReserved(Define),PIdnDef(inner_macro),None,PIntLit(42)) found" at "viper.silver.parser.TypeChecker.check(Resolver.scala:258)" (playground.vpr@2.1--11.2)

According to this specification: https://github.com/viperproject/silver/blob/master/documentation/syntax/sil-syntax.txt one should be able to define a macro inside another macro.

marcoeilers commented 3 months ago

Nested macro declarations actually shouldn't be allowed (I'll update the sil-syntax file separately). Since PR #795, nested macro declarations are rejected by the parser.