Skip to content

Introduce NameType#100

Open
The-Ray-Man wants to merge 5 commits intomainfrom
ramon/name-type
Open

Introduce NameType#100
The-Ray-Man wants to merge 5 commits intomainfrom
ramon/name-type

Conversation

@The-Ray-Man
Copy link
Copy Markdown
Collaborator

@The-Ray-Man The-Ray-Man commented Apr 9, 2026

This PR updates how we specify the name type. Before there was a string property mangledType on SymbolicName. This property describes what kind of entity the name refers to e.g. getter, property, function, type.

This strings should be duplicate free but they are distributed in many files. To have a better overview on the used strings a sealed class NameType was introduced which collects all the name types.

The changes in the resulting viper program can be categorized into:

  • type name update: Before the type of a function looked like this TF$T$Unit which was changed to t$F$t$Unit. Basically the upper case T was replaced with a lowercase to match the other type names. Also it was separated using $.
  • Label names changed slightly. E.g. try_exit to tryExit
  • Parameters in the type domain changed from arg1 to arg$1
  • Property getters type name is just g instead of pg
  • Predicates are prefixed with pred instead of p
  • Parameters are prefixed with par instead of p

Note: The NameType Special will be removed in a future PR. It makes sense to remove it, once we got rid off the SpecialName. Removing SpecialName requires a larger reconstruction.

@The-Ray-Man The-Ray-Man mentioned this pull request Apr 9, 2026
@The-Ray-Man The-Ray-Man self-assigned this Apr 9, 2026
@The-Ray-Man The-Ray-Man changed the title Introduce Name Type Introduce NameType Apr 9, 2026
@The-Ray-Man The-Ray-Man force-pushed the ramon/name-type branch 2 times, most recently from ec085d8 to e7a4b00 Compare April 9, 2026 13:14
@The-Ray-Man The-Ray-Man marked this pull request as ready for review April 9, 2026 16:00
@The-Ray-Man The-Ray-Man requested review from jesyspa and removed request for jesyspa April 10, 2026 07:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant