search

viperproject / silver

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

Add argument to properly disallow nested macros #795

Closed marcoeilers closed 3 months ago

marcoeilers commented 4 months ago

@JonasAlaif It looks to me as if the intention of the parser code is to disallow nested macro declarations (which would then prevent issues like #786), and the allowDefine value is just not properly forwarded in all cases in the stmtrule. Or am I mistaken and this is somehow in purpose?

JonasAlaif commented 3 months ago

From what I saw, yeah I think that that's the intention