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

"Crucible can only extract static methods" error from jvm_extract #1029

Open
brianhuffman opened this issue Jan 21, 2021 · 0 comments
Open

"Crucible can only extract static methods" error from jvm_extract #1029

brianhuffman opened this issue Jan 21, 2021 · 0 comments
Labels
regression Something that used to work, but now doesn't subsystem: crucible-jvm Issues related to Java verification with crucible-jvm tech debt Issues that document or involve technical debt type: bug Issues reporting bugs or unexpected/unwanted behavior
Milestone
Someday

Comments

@brianhuffman
Copy link
Contributor

brianhuffman commented Jan 21, 2021 •
edited
Loading

The jvm_extract command is more limited than the java_extract command that it is supposed to be replacing, because it only works for static methods. I believe it is also restricted to methods with argument and result types that are primitives, so it does not work with arrays either.

We need to bring the capabilities of jvm_extract up to par with java_extract before removing the older one (see #1005).
@brianhuffman brianhuffman added the subsystem: crucible-jvm Issues related to Java verification with crucible-jvm label Jan 21, 2021
@sauclovian-g sauclovian-g added type: bug Issues reporting bugs or unexpected/unwanted behavior tech debt Issues that document or involve technical debt regression Something that used to work, but now doesn't labels Oct 30, 2024
@sauclovian-g sauclovian-g added this to the Someday milestone Oct 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
regression Something that used to work, but now doesn't subsystem: crucible-jvm Issues related to Java verification with crucible-jvm tech debt Issues that document or involve technical debt type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Milestone
Someday
Development

No branches or pull requests
2 participants
@brianhuffman @sauclovian-g