viperproject / silver

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

Fixing issue #803 #804

Closed marcoeilers closed 3 months ago

marcoeilers commented 4 months ago

Fixing issue #803. The issue is that the macro expansion code that decides whether a variable has to be renamed because it clashes with a variable declared at the macro usage site sometimes claims that that variable names are used that actually aren't.

In particular, the code

That second step doesn't always work correctly, since there is a single set that keeps track of which names are added because of macro expansion. As a result, variable names that are added in one place as a result of a macro expansion count as used even in different scopes.

This PR fixes that by tracking which names are added per scope.