Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Construct a complete type checker for SharedTerm #1226

Closed
atomb opened this issue Aug 11, 2015 · 1 comment
Closed

Construct a complete type checker for SharedTerm #1226

atomb opened this issue Aug 11, 2015 · 1 comment
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem

Comments

@atomb
Copy link
Contributor

atomb commented Aug 11, 2015

The type checker in Verifier.SAW.SCTypeCheck is convenient, but not entirely complete. It can fail to type-check terms that are type correct. We should re-visit the design and either adapt it or replace it with something complete. However, the preferred mode of use should probably be to construct "certified" terms, as in GaloisInc/saw-core#18.
@brianhuffman brianhuffman transferred this issue from GaloisInc/saw-core Apr 27, 2021
@brianhuffman brianhuffman added the subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem label Apr 27, 2021
@brianhuffman
Copy link
Contributor

There has been a lot of work done on the SCTypeCheck module since 2015, and I expect that it's rather complete now. We can reopen if anyone comes across any specific examples of terms that should typecheck but don't.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@atomb @brianhuffman