-
Notifications
You must be signed in to change notification settings - Fork 33
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Shadowing builtin types in Alt-Ergo native language #1104
Comments
Note: it is easy for Dolmen to change that behavior and for instance treat as errors a problem that would try to redefine/shadow a builtin type (that is already being done for the smtlib). It all depends on the rules for the native ae language, which the alt-ergo team can choose. |
I think we should forbid such redefinitions but we can do it after the next release. |
IIRC it was used on function and value names, not on theory symbols, AFAIK the shadowing of theory symbols is not allowed in the SMT-LIB standard. |
Dolmen accepts to shadow some builtin types. For instance, the input file:
produces the error:
The legacy frontend of Alt-Ergo accepts this input file because it uses the names of types as identifiers.
Notice this file is refused by both legacy and Dolmen frontend:
because
int
is a reserved token, which isn't the case offarray
.It seems shadowing is used in the SMT-LIB as noticed in the issue #712.
The text was updated successfully, but these errors were encountered: