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

Unhelpful error message on read of uninitialized field by crucible_jvm_verify #925

Closed
brianhuffman opened this issue Nov 19, 2020 · 0 comments · Fixed by #981
Closed

Unhelpful error message on read of uninitialized field by crucible_jvm_verify #925

brianhuffman opened this issue Nov 19, 2020 · 0 comments · Fixed by #981
Assignees
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm topics: error-messages Issues involving the messages SAW produces on error
Milestone

Comments

@brianhuffman
Copy link
Contributor

When verifying a JVM method, it may happen that the symbolic tries to read an instance field or an array element, and fails because the value is uninitialized. (This may happen due to a missing points-to declaration in the method spec, for example.) But the error message when this happens is quite uninformative:

[20:19:53.913] Stack trace:
"crucible_jvm_verify" (/Users/huffman/Work/saw-script/intTests/test_jvm_method_names/test.saw:15:1-15:20):
Symbolic execution failed.
Abort due to false assumption:
  internal: error: in Test.get
  incorrect variant

It just says "incorrect variant", and doesn't give any clue about what caused the problem, what it was trying to do when it happened, or how to fix it.

In this case, the error occurred because it was trying to read the field called Test.val, of type long, but that field was uninitialized because I commented out the points-to precondition for that field in the SAW spec. The error message should at least include the name of the field it was trying to access.

@brianhuffman brianhuffman added subsystem: crucible-jvm Issues related to Java verification with crucible-jvm topics: error-messages Issues involving the messages SAW produces on error labels Nov 19, 2020
brianhuffman pushed a commit to GaloisInc/crucible that referenced this issue Nov 19, 2020
brianhuffman pushed a commit to GaloisInc/crucible that referenced this issue Nov 24, 2020
@brianhuffman brianhuffman self-assigned this Dec 2, 2020
@atomb atomb modified the milestones: 0.7, 0.8 Dec 11, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm topics: error-messages Issues involving the messages SAW produces on error
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants