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.

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

Signed version of prelude function toInteger #1266

Closed
brianhuffman opened this issue Aug 20, 2021 · 0 comments · Fixed by #1281
Closed

Signed version of prelude function toInteger #1266

brianhuffman opened this issue Aug 20, 2021 · 0 comments · Fixed by #1281
Assignees
Labels
language Changes or extensions to the language

Comments

@brianhuffman
Copy link
Contributor

The Cryptol prelude has a function toInteger that can convert a bitvector of type [n] to a non-negative integer in the range 0 to 2^^n-1. We need a signed variant of this function that converts a signed bitvector to an integer in the range -2^^(n-1) to 2^^(n-1)-1. Such a function exists in the saw prelude (called sbvToInt), but not in Cryptol.

@robdockins robdockins added the language Changes or extensions to the language label Sep 10, 2021
@brianhuffman brianhuffman self-assigned this Sep 10, 2021
@brianhuffman brianhuffman linked a pull request Sep 11, 2021 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
language Changes or extensions to the language
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants