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

JVM spec commands don't work with byte and char types #1006

Closed
brianhuffman opened this issue Jan 14, 2021 · 0 comments · Fixed by #1008
Closed

JVM spec commands don't work with byte and char types #1006

brianhuffman opened this issue Jan 14, 2021 · 0 comments · Fixed by #1008
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm

Comments

@brianhuffman
Copy link
Contributor

Using java type byte or char in a JVM spec with jvm_verify results in an error message like this:

resolveSAWTerm: unimplemented type char (FIXME)

We need to add support for these types in all the JVM verification commands.
@brianhuffman brianhuffman added the subsystem: crucible-jvm Issues related to Java verification with crucible-jvm label Jan 14, 2021
brianhuffman pushed a commit that referenced this issue Jan 15, 2021
Add support for small types (byte, char, short) in jvm verification.
5dec004 
Fixes #1006.
brianhuffman pushed a commit that referenced this issue Jan 15, 2021
Add integration test for #1006.
1948c21
@brianhuffman brianhuffman mentioned this issue Jan 15, 2021
Merged
brianhuffman pushed a commit that referenced this issue Jan 15, 2021
Add support for small types (byte, char, short) in jvm verification.
4602bc9 
Fixes #1006.
brianhuffman pushed a commit that referenced this issue Jan 15, 2021
Add integration test for #1006.
8aa4f53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Support byte/char/short in JVM verification commands. GaloisInc/saw-script
1 participant
@brianhuffman