search

viperproject / silver

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

goto name is replaced while label is not #787

Closed Bibin112358 closed 5 months ago

Bibin112358 commented 5 months ago

When defining a goto in a macro, its label is replaced, when it matches a macro argument. When defining a label in a macro, its label is not replaced, even if it matches a macro argument.

method main()
{
    m(some_name)
}

define m(label_name)
{
    goto label_name
    label label_name
}

I am not sure if that is intended or not.

marcoeilers commented 5 months ago

Fixed in #793