You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This issue is used to track the changes to the naming system.
FunctionTypeName, function types get their own name. It consists of the type of the arguments and the return type. Before the FunctionTypeEmbeddings name was just a list with the argument type names
Change field mangledType of SymbolicName to nameType: NameType. Created NameType to collect all the possible name types and their string representation in one place.
Created NamedEntity as an interface, it contains everything that has something to do with names. This includes: NameScope, NameType, and SymbolicName.
Create FreshName interface, to group the created fresh names (e.g. Label Names) together.
Create NameOfType interface, to group names together that describe a type.
During name registration to the name resolver, names declared in forall + exists are also registered. This is necessary, because in invariants we are not allowed to shadow local variables. Also we need to know the variables used during let expressions. Hence we need to traverse the full program.
Added the class ViperKeyword as a NamedEntity. All the keywords are collected in ViperKeywords
Introduce ShortNameResolver which when names are registered builds a dependency graph and focus on human readable names.
Renamed the axioms (now using camelCase instead of underscores). Was done, such that the same style is used throughout the typeDomain.
Changed SpecialName to a more fitting name: SpecialFieldName
Added RelatedDomainFuncName. This is a symbolic name that should be used for names of functions that are closely related to a domain but are not actually inside the domain.
Changed HavocKotlinName and PredicateKotlinName interface from KotlinName to SymbolicName. Since they could be scoped, changed the name parameter in ScopedKotlinName to SymbolicName
This issue is used to track the changes to the naming system.
FunctionTypeName, function types get their own name. It consists of the type of the arguments and the return type. Before theFunctionTypeEmbeddings name was just a list with the argument type namesmangledTypeofSymbolicNametonameType: NameType. CreatedNameTypeto collect all the possible name types and their string representation in one place.NamedEntityas an interface, it contains everything that has something to do with names. This includes:NameScope,NameType, andSymbolicName.FreshNameinterface, to group the created fresh names (e.g. Label Names) together.NameOfTypeinterface, to group names together that describe a type.forall+existsare also registered. This is necessary, because in invariants we are not allowed to shadow local variables. Also we need to know the variables used duringletexpressions. Hence we need to traverse the full program.ViperKeywordas aNamedEntity. All the keywords are collected inViperKeywordsShortNameResolverwhich when names are registered builds a dependency graph and focus on human readable names.SpecialNameto a more fitting name:SpecialFieldNameRelatedDomainFuncName. This is a symbolic name that should be used for names of functions that are closely related to a domain but are not actually inside the domain.HavocKotlinNameandPredicateKotlinNameinterface fromKotlinNametoSymbolicName. Since they could be scoped, changed the name parameter inScopedKotlinNametoSymbolicNameScopedKotlinNameto be justScopedName.Named Entity Hierarchy
NamedEntityNameScopeBadScopeClassScopeFakeScopeLocalScopePackageScopeParamterScopePrivateScopePublicScopeNameTypePropertyBackingFieldGetterSetterEtensionSetterEtensionGetterNameTypeClassConstructorFunctionPredicateHavocLabelReturnBreakContinueCatchTryEitVariablesDomainDomainFunctionSpecialSymbolicNameFreshNameAnonymousBuiltinNameAnonymousNameDispatchREceiverNameDomainFuncParameterNameEtensionREceiverNameFunctionResultVariableNameNumberedLabelNamePlaceholderArgumentNameReturnVariableNameSpecialNameSsaVariableNameKotlinNameClassKotlinNameConstructorKotlinNameSimpleKotlinNameTypedKotlinName(abstract)TypedKotlinNameWithTypeHavocNamePredicateNameScopedNameDomainNameNamedDomainAiomLabelQualifiedDomainFuncNameUnqualifiedDomainFuncNameNameOfTypeFunctionTypeNameListOfNamesPretypeNameTypeNameViperKeyword